English
For monotone f, ContinuityWithinAt f (Iio x) x is equivalent to leftLim f x = f x.
Русский
Для монотонной функции f непрерывность внутри Iio x в точке x эквивалентна равенству левой границы и значения функции: leftLim f x = f x.
LaTeX
$$$\operatorname{ContinuousWithinAt}(f,\mathrm{Iio}(x),x) \iff \operatorname{leftLim}(f,x) = f(x)$$$
Lean4
theorem leftLim_le (h : x ≤ y) : leftLim f x ≤ f y :=
by
letI : TopologicalSpace α := Preorder.topology α
haveI : OrderTopology α := ⟨rfl⟩
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
· simpa [leftLim, h'] using hf h
haveI A : NeBot (𝓝[<] x) := neBot_iff.2 h'
rw [leftLim_eq_sSup hf h']
refine csSup_le ?_ ?_
· simp only [image_nonempty]
exact (forall_mem_nonempty_iff_neBot.2 A) _ self_mem_nhdsWithin
· simp only [mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
intro z hz
exact hf (hz.le.trans h)
