subsingleton_isBot — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem subsingleton_isBot (α : Type*) [PartialOrder α] : {x : α | IsBot x}.Subsingleton := fun x hx _ hy =>
  hx.isMin.eq_of_ge (hy x)

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