noTopOrder — Mathlib

English

WithBot α has no top element, provided α has LE, NoTopOrder, and is nonempty.

Русский

WithBot α не имеет верхнего элемента при условии LE α, NoTopOrder α и непустоты α.

LaTeX

$$$NoTopOrder(WithBot \alpha)$$$

Lean4

instance noTopOrder [LE α] [NoTopOrder α] [Nonempty α] : NoTopOrder (WithBot α) where
  exists_not_le := fun
    | ⊥ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) =>
      let ⟨b, hba⟩ := exists_not_le a;
      ⟨b, mod_cast hba⟩

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