range_omega — Mathlib

English

The range of o ↦ ω_o equals the set { x | ω ≤ x and IsInitial x }.

Русский

Образ отображения o ↦ ω_o равен множеству { x | ω ≤ x и IsInitial(x) }.

LaTeX

$$$ \operatorname{range}(\omega) = \{ x \mid \omega \le x \wedge IsInitial(x) \}$$$

Lean4

@[simp]
theorem range_omega : range omega = {x | ω ≤ x ∧ IsInitial x} :=
  by
  ext x
  constructor
  · rintro ⟨a, rfl⟩
    exact ⟨omega0_le_omega a, isInitial_omega a⟩
  · rintro ⟨ha', ha⟩
    obtain ⟨a, rfl⟩ := ha.mem_range_preOmega
    use a - ω
    rw [omega0_le_preOmega_iff] at ha'
    rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']

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