denselyOrdered — Mathlib

English

If a is densely ordered with respect to the order <, then the dual order on a is also densely ordered; that is, between any two elements there exists a third element in the dual sense.

Русский

Если множество упорядочено плотно относительно порядка <, то двойственный порядок на этом множестве тоже плотно упорядочен; то есть между любыми двумя элементами в двойственной системе существует третий элемент.

LaTeX

$$$DenselyOrdered(\alpha^{\mathrm{op}})$$$

Lean4

instance denselyOrdered (α : Type*) [LT α] [h : DenselyOrdered α] : DenselyOrdered αᵒᵈ :=
  ⟨fun _ _ ha ↦ (@exists_between α _ h _ _ ha).imp fun _ ↦ And.symm⟩

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