term — Mathlib

English

An ordinal can be viewed as a term of I by assigning to each i its corresponding ordinal.

Русский

Ординал можно рассматривать как элемент множества I-термов, сопоставляя каждому i соответствующий ординал.

LaTeX

$$$\\text{An ordinal } o \\text{ is seen as a term } i \\in I \\text{ with } \\mathrm{ord}_I(i)=o.$$$

Lean4

/-- An ordinal regarded as a term of `I`. -/
noncomputable def term {o : Ordinal} (ho : o < Ordinal.type ((· < ·) : I → I → Prop)) : I :=
  Ordinal.enum ((· < ·) : I → I → Prop) ⟨o, ho⟩

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