English
If a function f has its left neighborhood image dense in a left neighborhood of f(a), then f is continuous at a from the left.
Русский
Если образ левой окрестности f(N) плотно лежит в левой окрестности f(a), то f непрерывна слева в a.
LaTeX
$$$\text{MonotoneOn}(f, s) \Rightarrow f'' s \text{ is dense near } f(a) \Rightarrow \text{ContinuousWithinAt}(f, \mathrm{Iic}(a), a)$$$
Lean4
/-- If `f` is a monotone function on a left neighborhood of `a` and the image of this neighborhood
under `f` meets every interval `(b, f a)`, `b < f a`, then `f` is continuous at `a` from the left.
The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)` cannot be replaced by the weaker
assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` we use for strictly monotone functions
because otherwise the function `floor : ℝ → ℤ` would be a counter-example at `a = 0`. -/
theorem continuousWithinAt_left_of_monotoneOn_of_exists_between {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s)
(hs : s ∈ 𝓝[≤] a) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)) : ContinuousWithinAt f (Iic a) a :=
@continuousWithinAt_right_of_monotoneOn_of_exists_between αᵒᵈ βᵒᵈ _ _ _ _ _ _ f s a hf.dual hs fun b hb =>
let ⟨c, hcs, hcb, hca⟩ := hfs b hb
⟨c, hcs, hca, hcb⟩
