preAleph_omega0

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Cardinal.preAleph_omega0

English

preAleph(ω) = ℵ₀.

Русский

preAleph(ω) = ℵ₀.

LaTeX

$$$ \text{preAleph}(\omega) = \aleph_0 $$$

Lean4

@[simp]
theorem preAleph_omega0 : preAleph ω = ℵ₀ := by rw [← card_preOmega, preOmega_omega0, card_omega0]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru