mem_range_omega_iff

Mathlib.SetTheory.Cardinal.Aleph

URI: https://scilib.ai/kg/mathlib#Ordinal.mem_range_omega_iff

English

An element x belongs to the range of ω if and only if x ≥ ω and x is initial.

Русский

Элемент x принадлежит диапазону ω тогда и только тогда, когда x ≥ ω и x начален.

LaTeX

$$$ x \in \operatorname{range}(\omega) \iff \omega \le x \land IsInitial(x) $$$

Lean4

theorem mem_range_omega_iff {x : Ordinal} : x ∈ range omega ↔ ω ≤ x ∧ IsInitial x := by rw [range_omega, mem_setOf]

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

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

Разделы

Аффилиация

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