countable_union

Mathlib.Data.Set.Countable

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

English

The union of two countable sets is countable.

Русский

Объединение двух счетных множеств счетно.

LaTeX

$$$\\operatorname{Countable}(s) \\wedge \\operatorname{Countable}(t) \\Rightarrow \\operatorname{Countable}(s \\cup t)$$$

Lean4

@[simp]
theorem countable_union {s t : Set α} : (s ∪ t).Countable ↔ s.Countable ∧ t.Countable := by
  simp [union_eq_iUnion, and_comm]

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

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

Разделы

Аффилиация

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