mk_Ioc_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_Ioc_real {a b : ℝ} (h : a < b) : #(Ioc a b) = 𝔠 :=
  le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Ioc_self)

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