rank_rat_real — Mathlib

English

The dimension of ℝ as a vector space over ℚ is the continuum cardinality: rank_ℚ(ℝ) = continuum.

Русский

Размерность ℝ как пространства над ℚ равна континууму: rank_ℚ(ℝ) = континуум.

LaTeX

$$$\\\\operatorname{rank}_{\\\\mathbb{Q}}\\\$\\\\mathbb{R}\\\$ = \\\\mathfrak{c}$$$

Lean4

@[simp]
theorem rank_rat_real : Module.rank ℚ ℝ = continuum :=
  by
  refine (Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real
  simpa [mk_real] using aleph0_lt_continuum

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