mk_Icc_real — Mathlib

English

For any real a < b, the half-open interval [a,b) has the cardinality of the continuum.

Русский

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

LaTeX

$$$\forall a,b \in \mathbb{R}, a < b \Rightarrow |[a,b)| = \mathfrak{c}$$$

Lean4

/-- The cardinality of the interval [a, b]. -/
theorem mk_Icc_real {a b : ℝ} (h : a < b) : #(Icc a b) = 𝔠 :=
  le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Icc_self)

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