ord — Mathlib

English

Define the ordinal type of an element i in I by comparing i with all smaller elements under the order < on I.

Русский

Определим ординал-тип элемента i∈I как типин-отрезок относительно порядка < на I.

LaTeX

$$$\\mathrm{ord}_I(i) := \\mathrm{Ordinal.typein}((<)_{I\\times I})\\; i.$$$

Lean4

/-- A term of `I` regarded as an ordinal. -/
def ord (i : I) : Ordinal :=
  Ordinal.typein ((· < ·) : I → I → Prop) i

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