mk_real — Mathlib

English

The real numbers have cardinality equal to the continuum.

Русский

Множество действительных чисел имеет кардинальность, равную континууму.

LaTeX

$$$|\mathbb{R}| = \mathfrak{c}$$$

Lean4

/-- The cardinality of the reals, as a type. -/
theorem mk_real : #ℝ = 𝔠 := by
  apply le_antisymm
  · rw [Real.equivCauchy.cardinal_eq]
    apply mk_quotient_le.trans
    apply (mk_subtype_le _).trans_eq
    rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
  · convert mk_le_of_injective (cantorFunction_injective _ _)
    · rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
    · exact 1 / 3
    · simp
    · norm_num

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