English
For monotone f and s, ContinuousWithinAt f s x is equivalent to continuity on s ∩ Iic x and s ∩ Ici x.
Русский
Для монотонной f и множества s непрерывность внутри s в x эквивалентна непрерывности на пересечении s с Iic x и s с Ici x.
LaTeX
$$$\operatorname{ContinuousWithinAt}(f,s,x) \iff \operatorname{ContinuousWithinAt}(f,s \cap \mathrm{Iic}(x), x) \land \operatorname{ContinuousWithinAt}(f,s \cap \mathrm{Ici}(x), x)$$$
Lean4
theorem le_leftLim (h : x < y) : f x ≤ leftLim f y :=
by
letI : TopologicalSpace α := Preorder.topology α
haveI : OrderTopology α := ⟨rfl⟩
rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
· rw [leftLim_eq_of_eq_bot _ h']
exact hf h.le
rw [leftLim_eq_sSup hf h']
refine le_csSup ⟨f y, ?_⟩ (mem_image_of_mem _ h)
simp only [upperBounds, mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
intro z hz
exact hf hz.le
