subsingleton_isTop — Mathlib

English

In any partially ordered set, the set of elements that are tops (IsTop x) is a subsingleton.

Русский

В любом частично упорядоченном множестве множество элементов, являющихся наивысшими (IsTop x), является подсинглтоном.

LaTeX

$$$ \forall \alpha \; [\text{PartialOrder }\alpha],\n\{x : \alpha \mid IsTop x\}.Subsingleton $$$

Lean4

theorem subsingleton_isTop (α : Type*) [PartialOrder α] : {x : α | IsTop x}.Subsingleton := fun x hx _ hy =>
  hx.isMax.eq_of_le (hy x)

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