denselyOrdered_range — Mathlib

English

If X is densely ordered and f: X → Y is strictly monotone, then the range of f is densely ordered in Y.

Русский

Если X плотно упорядочен, а f: X → Y строго монотонна, то множество значений f(X) плотно упорядочено внутри Y.

LaTeX

$$$ \operatorname{DenselyOrdered}(\operatorname{range}(f)) $$$

Lean4

theorem denselyOrdered_range {X Y : Type*} [LinearOrder X] [DenselyOrdered X] [Preorder Y] {f : X → Y}
    (hf : StrictMono f) : DenselyOrdered (Set.range f) :=
  by
  constructor
  simpa [← exists_and_left, ← exists_and_right, exists_comm, hf.lt_iff_lt] using fun _ _ ↦ exists_between

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