mk_Ici_real — Mathlib

English

For any real a, the interval [a, ∞) has the cardinality of the continuum.

Русский

Для любого действительного числа a кардинальность интервала [a, ∞) равна континууму.

LaTeX

$$$\#(Ici\ a) = \mathfrak{c}$$$

Lean4

/-- The cardinality of the interval [a, ∞). -/
theorem mk_Ici_real (a : ℝ) : #(Ici a) = 𝔠 :=
  le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioi_real a ▸ mk_le_mk_of_subset Ioi_subset_Ici_self)

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