continuous_of_denseRange — Mathlib

English

A monotone function with densely ordered codomain and dense range is continuous.

Русский

У монотонной функции с плотно упорядоченным кодом и плотным диапазоном вклад непрерывна.

LaTeX

$$$\\text{Monotone } f \\land \\text{DenseRange } f \\Rightarrow \\text{Continuous } f.$$$

Lean4

/-- A monotone function with densely ordered codomain and a dense range is continuous. -/
theorem continuous_of_denseRange [DenselyOrdered β] {f : α → β} (h_mono : Monotone f) (h_dense : DenseRange f) :
    Continuous f :=
  continuous_iff_continuousAt.mpr fun a =>
    continuousAt_of_monotoneOn_of_closure_image_mem_nhds (fun _ _ _ _ hxy => h_mono hxy) univ_mem <| by
      simp only [image_univ, h_dense.closure_eq, univ_mem]

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