aleph0_add_continuum — Mathlib

English

Let ℵ₀ denote the smallest infinite cardinal and 𝔠 denote the continuum. Then the sum of cardinals satisfies ℵ₀ + 𝔠 = 𝔠.

Русский

Пусть ℵ₀ обозначает наименьшую бесконечную кардинальность, а 𝔠 — континуум. Тогда сумма кардинальностей даёт 𝔠: ℵ₀ + 𝔠 = 𝔠.

LaTeX

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

Lean4

@[simp]
theorem aleph0_add_continuum : ℵ₀ + 𝔠 = 𝔠 :=
  add_eq_right aleph0_le_continuum aleph0_le_continuum

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