not_countable_iff

Mathlib.Data.Countable.Defs

URI: https://scilib.ai/kg/mathlib#not_countable_iff

English

For any α, not Countable α is equivalent to Uncountable α.

Русский

Для любого α не счётно тогда и только тогда, когда α неисчисляемо.

LaTeX

$$$\forall \alpha,\ (\neg \operatorname{Countable}(\alpha)) \iff \operatorname{Uncountable}(\alpha)$$$

Lean4

@[push]
theorem not_countable_iff : ¬Countable α ↔ Uncountable α :=
  (uncountable_iff_not_countable α).symm

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

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

Разделы

Аффилиация

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