denselyOrdered_iff — Mathlib

English

The dense-ordered nature with zero is equivalent to the underlying dense-ordered structure without zero.

Русский

Плотный порядок с нулем эквивалентен плотному порядку без нуля.

LaTeX

$$$\mathrm{DenselyOrdered}(\mathrm{WithZero}(M)) \iff \mathrm{DenselyOrdered}(M)$$$

Lean4

theorem denselyOrdered_iff {M : Type*} [Preorder M] [NoMinOrder M] : DenselyOrdered (WithZero M) ↔ DenselyOrdered M :=
  WithBot.denselyOrdered_iff

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