preAleph_pos

Mathlib.SetTheory.Cardinal.Aleph

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

English

0 < preAleph(o) ↔ 0 < o.

Русский

0 < preAleph(o) ⇔ 0 < o.

LaTeX

$$$ 0 < \text{preAleph}(o) \iff 0 < o $$$

Lean4

@[simp]
theorem preAleph_pos {o : Ordinal} : 0 < preAleph o ↔ 0 < o := by rw [← preAleph_zero, preAleph_lt_preAleph]

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

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

Разделы

Аффилиация

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