bfamilyOfFamily'_typein — Mathlib

English

If ι is well-ordered by r and f: ι → α, then evaluating the reindexed family on the canonical type-in index recovers f.

Русский

Если ι упорядочено по r и f: ι → α, то значение перерандексированного семейства на удобном представлении типа v возвращает f.

LaTeX

$$$\mathrm{bfamilyOfFamily'}(r,f)(\mathrm{typein}\, r\ i)(\mathrm{typein\_lt\_type}\, r\ i) = f\ i$$$

Lean4

@[simp]
theorem bfamilyOfFamily'_typein {ι} (r : ι → ι → Prop) [IsWellOrder ι r] (f : ι → α) (i) :
    bfamilyOfFamily' r f (typein r i) (typein_lt_type r i) = f i := by simp only [bfamilyOfFamily', enum_typein]

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