familyOfBFamily_enum — Mathlib

English

In the indexed reindexing by o, evaluating at the enum index yields f i hi as in the unindexed form.

Русский

При перерандексировании по o вычисления на enum-индексе дают f i hi в исходной форме.

LaTeX

$$$\mathrm{familyOfBFamily}(o,f)(\mathrm{enum}(\alpha := o.toType)(·<·)\langle i, hi.trans\_eq (type\_toType _).symm\rangle) = f i hi$$$

Lean4

theorem familyOfBFamily_enum (o : Ordinal) (f : ∀ a < o, α) (i hi) :
    familyOfBFamily o f (enum (α := o.toType) (· < ·) ⟨i, hi.trans_eq (type_toType _).symm⟩) = f i hi :=
  familyOfBFamily'_enum _ (type_toType o) f _ _

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