invVeblen₁_eq_iff — Mathlib

English

Let o be an ordinal. The equation invVeblen₁(o) = o holds exactly when either o = 0 or o lies in the range of Γ_.

Русский

Пусть o — ординал. Уравнение invVeblen₁(o) = o выполняется точно тогда, когда o = 0 или o принадлежит диапазону Γ_.

LaTeX

$$$$ invVeblen₁(o) = o \iff o = 0 \lor o \in \operatorname{range}(\Gamma_). $$$$

Lean4

theorem invVeblen₁_eq_iff : invVeblen₁ o = o ↔ o = 0 ∨ o ∈ range Γ_ :=
  by
  constructor
  · rw [mem_range_gamma, or_iff_not_imp_left]
    refine fun h ho ↦ (left_le_veblen ..).antisymm' ?_
    conv_rhs =>
      rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero, veblen_zero_apply, ←
        veblen_invVeblen₁_invVeblen₂, h]
    simp
  · aesop

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