noMaxOrder — Mathlib

English

In the dual order, NoMinOrder corresponds to NoMaxOrder in the original order.

Русский

В двойственном порядке отсутствие минимума соответствует отсутствию максимума в исходном порядке.

LaTeX

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

Lean4

instance noMaxOrder [LT α] [NoMinOrder α] : NoMaxOrder αᵒᵈ :=
  ⟨fun a => exists_lt (α := α) a⟩
    -- See note [lower instance priority]

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