enumOrd — Mathlib

English

The enumerator function enumOrd is defined as the least element of s above all previous enumerations: enumOrd(s)(o) = sInf (s ∩ {b | ∀ c<o, enumOrd(s)(c) < b}).

Русский

Перечислитель enumOrd(s) задаётся как наименьшее элемент множества s, который превосходит все значения предыдущих перечислений: enumOrd(s)(o) = sInf (s ∩ {b | ∀ c<o, enumOrd(s)(c) < b}).

LaTeX

$$$$ \\mathrm{enumOrd}(s)(o) = \\inf\\{\, b \\in s \\mid \\forall c

Lean4

/-- Enumerator function for an unbounded set of ordinals. -/
noncomputable def enumOrd (s : Set Ordinal.{u}) (o : Ordinal.{u}) : Ordinal.{u} :=
  sInf (s ∩ {b | ∀ c, c < o → enumOrd s c < b})
termination_by o

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