noMaxOrder — Mathlib

English

WithBot α has no maximal element, given LT α, NoMaxOrder α, and Nonempty α.

Русский

WithBot α не имеет максимального элемента при условии LT α, NoMaxOrder α и непустоты α.

LaTeX

$$$NoMaxOrder(WithBot \alpha)$$$

Lean4

instance noMaxOrder [LT α] [NoMaxOrder α] [Nonempty α] : NoMaxOrder (WithBot α) where
  exists_gt := fun
    | ⊥ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) =>
      let ⟨b, hba⟩ := exists_gt a;
      ⟨b, mod_cast hba⟩

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