English
For any real a < b, the 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_Ioo_real {a b : ℝ} (h : a < b) : #(Ioo a b) = 𝔠 :=
by
refine le_antisymm (mk_real ▸ mk_set_le _) ?_
have h1 : #((fun x => x - a) '' Ioo a b) ≤ #(Ioo a b) := mk_image_le
refine le_trans ?_ h1
rw [image_sub_const_Ioo, sub_self]
replace h := sub_pos_of_lt h
have h2 : #(Inv.inv '' Ioo 0 (b - a)) ≤ #(Ioo 0 (b - a)) := mk_image_le
refine le_trans ?_ h2
rw [image_inv_eq_inv, inv_Ioo_0_left h, mk_Ioi_real]
