strictMono_of_inj_boundedOrder' — Mathlib

English

If α is a densely ordered, conditionally complete linear order and f is continuous and injective, then f is strictly monotone or strictly antitone.

Русский

Пусть α — плотно упорядоченный условно завершенный линейный порядок, и f непрерывна и инъективна; тогда f строго монотонна или строго антимонотонна.

LaTeX

$$StrictMono f ∨ StrictAnti f$$

Lean4

theorem strictMono_of_inj_boundedOrder' [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf_i : Injective f) :
    StrictMono f ∨ StrictAnti f :=
  (le_total (f ⊥) (f ⊤)).imp (hf_c.strictMono_of_inj_boundedOrder · hf_i) (hf_c.strictAnti_of_inj_boundedOrder · hf_i)

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