finite_isBot — Mathlib

English

For any partial order α, the set of bottom elements {a ∈ α | IsBot a} is finite (in fact a subsingleton).

Русский

Для частичного порядка α множество нижних элементов {a ∈ α | IsBot a} конечное (на самом деле — пододнозначное).

LaTeX

$$$\{a \in \alpha \mid \text{IsBot}(a)\}.\text{Finite}$$$

Lean4

theorem finite_isBot : {a : α | IsBot a}.Finite :=
  (subsingleton_isBot α).finite

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