mk_union_le_aleph0 — Mathlib

English

For sets P and Q, P ∪ Q is countable if and only if both P and Q are countable.

Русский

Объединение двух множеств счетно тогда и только тогда, когда оба множества счетны.

LaTeX

$$$|P \\cup Q| \\le \\aleph_0 \\;\\iff\\; |P| \\le \\aleph_0 \\land |Q| \\le \\aleph_0$$$

Lean4

theorem mk_union_le_aleph0 {α} {P Q : Set α} : #(P ∪ Q : Set α) ≤ ℵ₀ ↔ #P ≤ ℵ₀ ∧ #Q ≤ ℵ₀ := by
  simp only [le_aleph0_iff_subtype_countable, setOf_mem_eq, Set.union_def, ← countable_union]

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