range_aleph — Mathlib

English

range aleph equals Set.Ici ℵ₀ (i.e., cardinals at least ℵ₀).

Русский

Область определения aleph совпадает с множеством кардиналов не меньше ℵ₀.

LaTeX

$$$$ \operatorname{range}(\aleph) = \{ c \mid c \ge \aleph_{0} \}. $$$$

Lean4

@[simp]
theorem range_aleph : range aleph = Set.Ici ℵ₀ := by
  ext c
  refine ⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩
  rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]
  rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

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