mk_univ_real — Mathlib

English

The cardinality of the full real universe Set.univ is the continuum.

Русский

Кардинальность множества Set.univ, являющегося вселенной для действительных чисел, равна континууму.

LaTeX

$$$|\mathrm{Set.univ} : \mathrm{Set}\,\mathbb{R}| = \mathfrak{c}$$$

Lean4

/-- The cardinality of the reals, as a set. -/
theorem mk_univ_real : #(Set.univ : Set ℝ) = 𝔠 := by rw [mk_univ, mk_real]

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