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 α
h' : 𝓝[Iio x] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = 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 α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = 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 α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = 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 α
h' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = 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 α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 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 α
h' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) 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 α
h' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
refine' ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun 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 α
h' : 𝓝[Iio x] x ≠ ⊥
this✝ : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
this : Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) 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 α
h' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x
have := hf.tendsto_leftLim x
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 α
h' : 𝓝[Iio x] x ≠ ⊥
this✝ : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
this : Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x
rwa [h] at this
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 α
h' : 𝓝[Iio x] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
simp [leftLim_eq_of_eq_bot f h', ContinuousWithinAt, h']