ord_term — Mathlib

English

For any o and ho with o < type(...), ord I i = o if and only if term I ho = i.

Русский

Для любых o и ho, если o < type(...), то ord I i = o тогда и только тогда, когда term I ho = i.

LaTeX

$$$\\forall o, ho:\\ o<\\mathrm{type}((<)) \\Rightarrow\\forall i:\\mathrm{ord}_I(i)=o \\iff \\mathrm{term}_I(ho)=i.$$$

Lean4

theorem ord_term {o : Ordinal} (ho : o < Ordinal.type ((· < ·) : I → I → Prop)) (i : I) : ord I i = o ↔ term I ho = i :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · subst h
    exact term_ord_aux ho
  · subst h
    exact ord_term_aux ho

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