Theorem: le_iSup_of_tendsto (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ a ≤ iSup f
Tactic:
apply le_of_forall_lt
State after:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ ∀ c < a, c < iSup f

State before:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ ∀ c < a, c < iSup f
Tactic:
intro c hc
State after:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
⊢ c < iSup f

State before:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
⊢ c < iSup f
Tactic:
have : ∀ᶠ (x : β) in atTop, c < f x := by
  apply eventually_gt_of_tendsto_gt hc ha
State after:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
⊢ c < iSup f

State before:
case H
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
⊢ c < iSup f
Tactic:
rcases this.exists with ⟨x, hx⟩
State after:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ c < iSup f

State before:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ c < iSup f
Tactic:
apply lt_of_lt_of_le hx
State after:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ f x ≤ iSup f

State before:
case H.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
this : ∀ᶠ (x : β) in atTop, c < f x
x : β
hx : c < f x
⊢ f x ≤ iSup f
Tactic:
apply le_iSup
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
ha : Tendsto f atTop (𝓝 a)
c : α
hc : c < a
⊢ ∀ᶠ (x : β) in atTop, c < f x
Tactic:
apply eventually_gt_of_tendsto_gt hc ha
State after:
no goals