continuum_add_aleph0 — Mathlib

English

If a set has the cardinality of the continuum and another set has cardinality at most continuum, their union has cardinality equal to the continuum. In particular, 𝔠 + ℵ₀ = 𝔠.

Русский

Если множество имеет кардинальность континуума, а другое множество не превосходит континуум по кардинальности, то их объединение имеет кардинальность континуум. Особенно, 𝔠 + ℵ₀ = 𝔠.

LaTeX

$$$\mathfrak{c} + \aleph_0 = \mathfrak{c}$$$

Lean4

@[simp]
theorem continuum_add_aleph0 : 𝔠 + ℵ₀ = 𝔠 :=
  (add_comm _ _).trans aleph0_add_continuum

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