isTop — Mathlib

English

Let α be a preorder and subsingleton. Then every a ∈ α is the top element: IsTop a (i.e., ∀ x, x ≤ a).

Русский

Пусть α — множество с порядком и субоднозначно. Тогда любой элемент a ∈ α является верхним элементом: IsTop a (то есть ∀ x, x ≤ a).

LaTeX

$$$\\forall {\\alpha : Type*} [Preorder \\alpha] [Subsingleton \\alpha] (a : \\alpha), IsTop a$$$

Lean4

protected theorem isTop (a : α) : IsTop a := fun _ => (Subsingleton.elim _ _).le

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