mk_Ico_real — Mathlib

English

For all real a < b, the cardinality of the open interval (a,b) is 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_Ico_real {a b : ℝ} (h : a < b) : #(Ico a b) = 𝔠 :=
  le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Ico_self)

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