[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SupConvergenceClass α
[PROOFSTEP]
refine' ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => _, fun b hb => _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, b < CoeTC.coe b_1
[PROOFSTEP]
rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : α
hcs : c ∈ s
bc : b < c
bca : c ≤ a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, b < CoeTC.coe b_1
[PROOFSTEP]
lift c to s using hcs
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : { x // x ∈ s }
bc : b < ↑c
bca : ↑c ≤ a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, b < CoeTC.coe b_1
[PROOFSTEP]
refine' (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, CoeTC.coe b_1 < b
[PROOFSTEP]
exact eventually_of_forall fun x => (ha.1 x.2).trans_lt hb
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)
[PROOFSTEP]
suffices : Tendsto (rangeFactorization f) atTop atTop
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
this : Tendsto (rangeFactorization f) atTop atTop
⊢ Tendsto f atTop (𝓝 a)
case this
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
[PROOFSTEP]
exact (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
[PROOFSTEP]
exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsLUB (range f) a
⊢ Tendsto f atBot (𝓝 a)
[PROOFSTEP]
convert tendsto_atTop_isLUB h_anti.dual_left ha using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsGLB (range f) a
⊢ Tendsto f atBot (𝓝 a)
[PROOFSTEP]
convert tendsto_atTop_isLUB h_mono.dual ha.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto f atTop (𝓝 a)
[PROOFSTEP]
convert tendsto_atBot_isLUB h_anti.dual ha.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : IsEmpty ι
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : Nonempty ι
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
[PROOFSTEP]
exacts [tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_ciSup hbdd)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
hbdd : BddAbove (range f)
⊢ Tendsto f atBot (𝓝 (⨆ (i : ι), f i))
[PROOFSTEP]
convert tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddBelow (range f)
⊢ Tendsto f atBot (𝓝 (⨅ (i : ι), f i))
[PROOFSTEP]
convert tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ (i : ι), f i))
[PROOFSTEP]
convert tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
⊢ SupConvergenceClass (α × β)
[PROOFSTEP]
constructor
[GOAL]
case tendsto_coe_atTop_isLUB
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
⊢ ∀ (a : α × β) (s : Set (α × β)), IsLUB s a → Tendsto CoeTC.coe atTop (𝓝 a)
[PROOFSTEP]
rintro ⟨a, b⟩ s h
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB s (a, b)
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
rw [isLUB_prod, ← range_restrict, ← range_restrict] at h 
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (restrict s fst)) (a, b).fst ∧ IsLUB (range (restrict s snd)) (a, b).snd
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
have A : Tendsto (fun x : s => (x : α × β).1) atTop (𝓝 a) := tendsto_atTop_isLUB (monotone_fst.restrict s) h.1
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (restrict s fst)) (a, b).fst ∧ IsLUB (range (restrict s snd)) (a, b).snd
A : Tendsto (fun x => (↑x).fst) atTop (𝓝 a)
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) := tendsto_atTop_isLUB (monotone_snd.restrict s) h.2
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (restrict s fst)) (a, b).fst ∧ IsLUB (range (restrict s snd)) (a, b).snd
A : Tendsto (fun x => (↑x).fst) atTop (𝓝 a)
B : Tendsto (fun x => (↑x).snd) atTop (𝓝 b)
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
convert A.prod_mk_nhds B
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
⊢ SupConvergenceClass ((i : ι) → α i)
[PROOFSTEP]
refine' ⟨fun f s h => _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : IsLUB s f
⊢ Tendsto CoeTC.coe atTop (𝓝 f)
[PROOFSTEP]
simp only [isLUB_pi, ← range_restrict] at h 
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : ∀ (a : ι), IsLUB (range (restrict s (eval a))) (f a)
⊢ Tendsto CoeTC.coe atTop (𝓝 f)
[PROOFSTEP]
exact tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).restrict _) (h i)
[GOAL]
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto (f ∘ φ) atTop (𝓝 l) → Tendsto f atTop (𝓝 l)
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)
[PROOFSTEP]
exact h.comp hg
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)
[PROOFSTEP]
rcases tendsto_of_monotone hf with (h' | ⟨l', hl'⟩)
[GOAL]
case mpr.inl
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
h' : Tendsto f atTop atTop
⊢ Tendsto f atTop (𝓝 l)
[PROOFSTEP]
exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim
[GOAL]
case mpr.inr.intro
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l)
[PROOFSTEP]
rwa [tendsto_nhds_unique h (hl'.comp hg)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ IsLUB (range f) a
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case left.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a
[PROOFSTEP]
exact hf.ge_of_tendsto ha b
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))
[PROOFSTEP]
exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)
