IsFundamentalSequence — Mathlib

English

Definition: A fundamental sequence for a is an increasing sequence f on o with o ≤ cof(a).ord and blsub(o,f)=a.

Русский

Определение: фундаментальная последовательность для a — возрастающая последовательность f длины o, где o ≤ cof(a).ord и blsub(o,f)=a.

LaTeX

$$$$\text{IsFundamentalSequence}(a,o,f)\;:\; o\le a.cof.ord \wedge (\forall i

Lean4

/-- A fundamental sequence for `a` is an increasing sequence of length `o = cof a` that converges at
    `a`. We provide `o` explicitly in order to avoid type rewrites. -/
def IsFundamentalSequence (a o : Ordinal.{u}) (f : ∀ b < o, Ordinal.{u}) : Prop :=
  o ≤ a.cof.ord ∧ (∀ {i j} (hi hj), i < j → f i hi < f j hj) ∧ blsub.{u, u} o f = a

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