continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin

English

If a function has a left neighborhood mapping that meets left intervals densely, then continuity on the left holds.

Русский

Если отображение левой окрестности попадает в интервалы слева плотно, то непрерывность слева сохраняется.

LaTeX

$$$\text{MonotoneOn}(f, s) \Rightarrow f'' s \text{ meets left intervals densely} \Rightarrow \text{ContinuousWithinAt}(f, \mathrm{Iic}(a), a)$$$

Lean4

/-- If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and
the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is continuous at
`a` from the left. -/
theorem continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin [DenselyOrdered β] {f : α → β} {s : Set α} {a : α}
    (h_mono : MonotoneOn f s) (hs : s ∈ 𝓝[≤] a) (hfs : f '' s ∈ 𝓝[≤] f a) : ContinuousWithinAt f (Iic a) a :=
  continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono hs (mem_of_superset hfs subset_closure)

Похожие утверждения