familyOfBFamily'_enum — Mathlib

English

For a well-order ι with r and ho: type r = o, and f: ∀ a < o, α, evaluating the primed reindexed family at the enum index gives f i hi.

Русский

Пусть ι упорядочено р и ho: type r = o; тогда при вычислении перерандексированного семейства по enum получается f i hi.

LaTeX

$$$\mathrm{familyOfBFamily'}\ r\ ho\ f(\mathrm{enum}\ r\langle i,\cdots\rangle) = f\ i\ hi$$$

Lean4

theorem familyOfBFamily'_enum {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o) (f : ∀ a < o, α)
    (i hi) : familyOfBFamily' r ho f (enum r ⟨i, by rwa [ho]⟩) = f i hi := by simp only [familyOfBFamily', typein_enum]

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