countable_isTop

Mathlib.Data.Set.Countable

URI: https://scilib.ai/kg/mathlib#Set.countable_isTop

English

In any partially ordered set, the set of top elements is countable.

Русский

В частично упорядоченном множестве множество верхних элементов счётно.

LaTeX

$$$\\operatorname{Countable}\\big\\{ x\\in \\alpha \\mid \\operatorname{IsTop}(x) \\big\\}.$$$

Lean4

theorem countable_isTop (α : Type*) [PartialOrder α] : {x : α | IsTop x}.Countable :=
  (finite_isTop α).countable

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru