isBot — Mathlib

English

Let α be a preorder and assume α is a subsingleton. Then every element a ∈ α is a bottom element: IsBot a (i.e., a ≤ x for all x ∈ α).

Русский

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

LaTeX

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

Lean4

protected theorem isBot (a : α) : IsBot a := fun _ => (Subsingleton.elim _ _).le

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