not_isMax — Mathlib

English

In a nontrivial preorder, a bottom element cannot be a top element.

Русский

В неединственном порядке нижний элемент не может быть верхним.

LaTeX

$$$\\forall {\\alpha : Type*} [PartialOrder \\alpha] [Nontrivial \\alpha] (a : \\alpha), IsBot a \\rightarrow \\neg IsMax a$$$

Lean4

protected theorem not_isMax [Nontrivial α] (ha : IsBot a) : ¬IsMax a :=
  by
  intro ha'
  obtain ⟨b, hb⟩ := exists_ne a
  exact hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le

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