blsub — Mathlib

English

The bounded lower-substitution (blsub) is defined as the least strict upper bound of the family of successors of f restricted to a<o.

Русский

Определение blsub: наименьшая строгая верхняя граница семейства succ(f(a)) для a<o.

LaTeX

$$def blsub (o : Ordinal) (f : ∀ a < o, Ordinal) : Ordinal := bsup o (λ a ha => succ (f a ha))$$

Lean4

/-- The least strict upper bound of a family of ordinals indexed by the set of ordinals less than
    some `o : Ordinal.{u}`.

    This is to `lsub` as `bsup` is to `sup`. -/
def blsub (o : Ordinal.{u}) (f : ∀ a < o, Ordinal.{max u v}) : Ordinal.{max u v} :=
  bsup.{_, v} o fun a ha => succ (f a ha)

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