continuousAt_of_monotoneOn_of_image_mem_nhds

English

If f is monotone on a neighborhood s of a and s ∈ nhds a and Set.image f s ∈ nhds (f a), then f is continuous at a.

Русский

Если f монотонна на окрестности s точки a и s ∈ nhds a, а образ Set.image f s ∈ nhds (f a), то f непрерывна в a.

LaTeX

$$$(\\text{MonotoneOn } f s) \\land s \\in nhds a \\land Set.image f s \\in nhds (f a) \\Rightarrow ContinuousAt f a.$$$

Lean4

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

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