tendsto_atTop_isLUB — Mathlib

English

A monotone surjective function with densely ordered codomain is continuous.

Русский

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

LaTeX

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

Lean4

theorem tendsto_atTop_isLUB (h_mono : Monotone f) (ha : IsLUB (Set.range f) a) : Tendsto f atTop (𝓝 a) :=
  by
  suffices Tendsto (rangeFactorization f) atTop atTop from
    (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
  exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge

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