denselyOrdered_orderDual — Mathlib

English

Density is preserved by taking the order dual: DenselyOrdered(αᵒᵈ) iff DenselyOrdered(α).

Русский

Плотность сохраняется при переходе к двойственному порядку: DenselyOrdered(αᵒᵈ) эквивалентно DenselyOrdered(α).

LaTeX

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

Lean4

@[simp]
theorem denselyOrdered_orderDual [LT α] : DenselyOrdered αᵒᵈ ↔ DenselyOrdered α :=
  ⟨by convert @OrderDual.denselyOrdered αᵒᵈ _, @OrderDual.denselyOrdered α _⟩

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