derivFamily_limit — Mathlib

English

If o is a successor-limit ordinal, then the derivative at o is the supremum of the derivatives at all b with b < o: derivFamily f o = ⨆ b : Set.Iio o, derivFamily f b.

Русский

Если o является предельным по отношению к succ, то производная в o равна верхней границе всех значений derivFamily f b, где b < o: derivFamily f o = ⨆ b : Set.Iio o, derivFamily f b.

LaTeX

$$$$ IsSuccLimit(o) \rightarrow derivFamily f o = \bigvee_{b \in \mathrm{Iio}(o)} derivFamily f b. $$$$

Lean4

theorem derivFamily_limit (f : ι → Ordinal → Ordinal) {o} :
    IsSuccLimit o → derivFamily f o = ⨆ b : Set.Iio o, derivFamily f b :=
  limitRecOn_limit _ _ _ _

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