continuous_of_surjective — Mathlib

English

A monotone function with a densely ordered codomain that is surjective is continuous.

Русский

Монотонная функция с плотным порядком кодом и сюръективная непрерывна.

LaTeX

$$$\\text{Monotone } f \\Rightarrow \\text{Function.Surjective } f \\Rightarrow \\text{Continuous } f.$$$

Lean4

/-- A monotone surjective function with a densely ordered codomain is continuous. -/
theorem continuous_of_surjective [DenselyOrdered β] {f : α → β} (h_mono : Monotone f) (h_surj : Function.Surjective f) :
    Continuous f :=
  h_mono.continuous_of_denseRange h_surj.denseRange

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