le_aleph0_iff_subtype_countable

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.le_aleph0_iff_subtype_countable

English

For any predicate p on α, #{ x // p x } ≤ aleph0 if and only if {x | p x}.Countable.

Русский

Для предиката p на α, #{ x // p x } ≤ aleph0 тогда и только тогда {x | p x}.Countable.

LaTeX

$$$ #{ x // p x } \le \aleph_0 \iff {x | p x}.Countable $$$

Lean4

@[simp]
theorem le_aleph0_iff_subtype_countable {p : α → Prop} : #{ x // p x } ≤ ℵ₀ ↔ {x | p x}.Countable :=
  le_aleph0_iff_set_countable

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

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

Разделы

Аффилиация

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