of_subsingleton

Mathlib.Data.Set.Countable

URI: https://scilib.ai/kg/mathlib#Set.Countable.of_subsingleton

English

If α is a subsingleton, any subset s of α is countable.

Русский

Если α — субоднозначное множество, любое подмножество s ⊆ α счётно.

LaTeX

$$$[\\text{Subsingleton }\\alpha]\\quad \\forall s: Set\\alpha,\\operatorname{Countable}(s).$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton α] (s : Set α) : s.Countable :=
  (Finite.of_subsingleton s).countable

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

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

Разделы

Аффилиация

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