instNoBotOrderOfNoMinOrder — Mathlib

English

If α has NoMinOrder, then NoBotOrder α holds; equivalently, for every a, there exists b with b < a.

Русский

Если в α нет минимума, то выполняется отсутствие нижнего элемента; для любого a существует b, такой что b < a.

LaTeX

$$$\text{NoMinOrder}(\alpha) \Rightarrow \text{NoBotOrder}(\alpha)$$$

Lean4

instance (priority := 100) [Preorder α] [NoMinOrder α] : NoBotOrder α :=
  ⟨fun a => (exists_lt a).imp fun _ => not_le_of_gt⟩
    -- See note [lower instance priority]

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