of_forall_eq_top — Mathlib

English

If every element a with a ≠ ⊥ satisfies a = ⊤, then the order is simple; equivalently, for every a, a = ⊥ or a = ⊤.

Русский

Если для каждого элемента a выполняется a ≠ ⊥ ⇒ a = ⊤, то порядок прост; эквивалентно тому, что для каждого a выполняется a = ⊥ или a = ⊤.

LaTeX

$$$\forall a:\alpha,\ a=a=⊥ \lor a=⊤$$$

Lean4

theorem of_forall_eq_top {α : Type*} [LE α] [BoundedOrder α] [Nontrivial α] (h : ∀ a : α, a ≠ ⊥ → a = ⊤) :
    IsSimpleOrder α where eq_bot_or_eq_top a := or_iff_not_imp_left.mpr <| h a

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