union

Mathlib.Data.Set.Countable

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

English

(\n The same as countable_union; union of two countable sets is countable.

Русский

То же что и предыдущее.

LaTeX

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

Lean4

theorem union {s t : Set α} (hs : s.Countable) (ht : t.Countable) : (s ∪ t).Countable :=
  countable_union.2 ⟨hs, ht⟩

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

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

Разделы

Аффилиация

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