instDenselyOrdered — Mathlib

English

If α is a Preorder with DenseOrder, then the upper set { x ∈ α : a ≤ x } is densely ordered.

Русский

Если α имеет плотный порядок (DenseOrder), то верхнее множество { x ∈ α : a ≤ x } также плотно упорядочено.

LaTeX

$$$\\forall x,y \\in \\alpha,\\ a \\le x < y \\Rightarrow \\exists z \\in \\alpha\\ (a \\le x < z < y)$$$

Lean4

instance instDenselyOrdered [Preorder α] [DenselyOrdered α] {a : α} : DenselyOrdered { x : α // a ≤ x } :=
  show DenselyOrdered (Ici a) from Set.instDenselyOrdered

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