instDenselyOrderedWithZeroOfNoMinOrder

English

If X has no minimal element and is densely ordered, then WithZero X is densely ordered.

Русский

Если у X нет минимума и он плотно упорядочен, то WithZero X также плотно упорядочено.

LaTeX

$$$\text{DenselyOrdered}(X) \Rightarrow \text{DenselyOrdered}(\mathrm{WithZero}(X))$$$

Lean4

instance {X : Type*} [Preorder X] [NoMinOrder X] [DenselyOrdered X] : DenselyOrdered (WithZero X) :=
  WithZero.denselyOrdered_iff.mpr inferInstance

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