denselyOrdered_iff — Mathlib

English

Under LT α and NoMaxOrder α, densely ordered WithTop α is equivalent to densely ordered α.

Русский

При LT α и NoMaxOrder α условие плотности WithTop α эквивалентно плотности α.

LaTeX

$$$\\operatorname{DenselyOrdered}(\\mathrm{WithTop}\\,\\alpha) \\iff \\operatorname{DenselyOrdered}(\\alpha)$$$

Lean4

theorem denselyOrdered_iff [LT α] [NoMaxOrder α] : DenselyOrdered (WithTop α) ↔ DenselyOrdered α :=
  by
  rw [← denselyOrdered_orderDual, iff_comm, ← denselyOrdered_orderDual]
  exact WithBot.denselyOrdered_iff.symm

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