mk_Iio_real — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The cardinality of the interval (-∞, a). -/
theorem mk_Iio_real (a : ℝ) : #(Iio a) = 𝔠 :=
  by
  refine le_antisymm (mk_real ▸ mk_set_le _) ?_
  have h2 : (fun x => a + a - x) '' Iio a = Ioi a := by simp only [image_const_sub_Iio, add_sub_cancel_right]
  exact mk_Ioi_real a ▸ h2 ▸ mk_image_le

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