isNormal_iff_strictMono_and_continuous

English

IsNormal f iff f is strictly monotone and continuous.

Русский

IsNormal f эквивалентно тому, что f строго монотонна и непрерывна.

LaTeX

$$IsNormal f ↔ StrictMono f ∧ Continuous f$$

Lean4

@[deprecated Order.isNormal_iff_strictMono_and_continuous (since := "2025-08-21")]
theorem isNormal_iff_strictMono_and_continuous (f : Ordinal.{u} → Ordinal.{u}) :
    IsNormal f ↔ StrictMono f ∧ Continuous f :=
  Order.isNormal_iff_strictMono_and_continuous

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