noBotOrder — Mathlib

English

If α has a linear order with NoTopOrder, then the dual order αᵒᵈ has NoBotOrder.

Русский

Если у α есть линейный порядок без верхнего элемента, то в двойственном порядке αᵒᵈ существует отсутствие нижнего элемента.

LaTeX

$$$\text{NoTopOrder}(\alpha) \Rightarrow \text{NoBotOrder}(\alpha^{\mathrm{op}})$$$

Lean4

instance noBotOrder [LE α] [NoTopOrder α] : NoBotOrder αᵒᵈ :=
  ⟨fun a => exists_not_le (α := α) a⟩

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