instNoTopOrderOfNoMaxOrder — Mathlib

English

If α has NoMaxOrder, then the dual order αᵒᵈ has NoTopOrder.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) [Preorder α] [NoMaxOrder α] : NoTopOrder α :=
  ⟨fun a => (exists_gt a).imp fun _ => not_le_of_gt⟩

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