finite_isTop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem finite_isTop : {a : α | IsTop a}.Finite :=
  (subsingleton_isTop α).finite

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