case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x = ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (sSup (f '' Iio x)))
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
rw [leftLim_eq_sSup hf h']
no goals
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (sSup (f '' Iio x)))
exact hf.tendsto_nhdsWithin_Iio x
no goals
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x = ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
simp [h']