English
For any real a, the interval (a, ∞) has the cardinality of the continuum.
Русский
Для любого действительного числа a кардинальность интервала (a, ∞) равна континууму.
LaTeX
$$$\#(Ioi\ a) = \mathfrak{c}$$$
Lean4
/-- The cardinality of the interval (a, ∞). -/
theorem mk_Ioi_real (a : ℝ) : #(Ioi a) = 𝔠 :=
by
refine le_antisymm (mk_real ▸ mk_set_le _) ?_
rw [← not_lt]
intro h
refine _root_.ne_of_lt ?_ mk_univ_real
have hu : Iio a ∪ { a } ∪ Ioi a = Set.univ :=
by
convert @Iic_union_Ioi ℝ _ _
exact Iio_union_right
rw [← hu]
grw [mk_union_le, mk_union_le]
have h2 : (fun x => a + a - x) '' Ioi a = Iio a :=
by
convert @image_const_sub_Ioi ℝ _ _ _
simp
rw [← h2]
refine add_lt_of_lt (cantor _).le ?_ h
refine add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) ?_
rw [mk_singleton]
exact one_lt_aleph0.trans (cantor _)
