fact_isRegular_aleph0

Mathlib.SetTheory.Cardinal.Regular

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

English

Fact that aleph0 is regular.

Русский

Факт того, что aleph0 регулярен.

LaTeX

$$Fact(IsRegular(aleph0)).$$

Lean4

theorem fact_isRegular_aleph0 : Fact (IsRegular ℵ₀) where out := isRegular_aleph0

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

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

Разделы

Аффилиация

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