case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
⊢ f x ≤ b
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ b ∈ upperBounds (f '' s)
rintro _ ⟨x, hx, rfl⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
⊢ f x ≤ b
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
⊢ f x ≤ b
replace ha := ha.inter_Ici_of_mem hx
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : NeBot (𝓝[s ∩ Ici x] a)
⊢ f x ≤ b
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
⊢ f x ≤ b
haveI := ha.nhdsWithin_neBot ⟨x, hx, le_rfl⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : NeBot (𝓝[s ∩ Ici x] a)
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : NeBot (𝓝[s ∩ Ici x] a)
⊢ f x ≤ b
refine' ge_of_tendsto (hb.mono_left (nhdsWithin_mono _ (inter_subset_left s (Ici x)))) _
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁸ : TopologicalSpace α
inst✝⁷ : TopologicalSpace β
inst✝⁶ : LinearOrder α
inst✝⁵ : LinearOrder β
inst✝⁴ : OrderTopology α
inst✝³ : OrderTopology β
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
this : NeBot (𝓝[s ∩ Ici x] a)
⊢ ∀ᶠ (c : α) in 𝓝[s ∩ Ici x] a, f x ≤ f c
exact mem_of_superset self_mem_nhdsWithin fun y hy => hf hx hy.1 hy.2