bfamilyOfFamily_typein — Mathlib

English

For any i, the reindexed family built from f evaluated at typein i with typein_lt_type i equals f i.

Русский

Для любого i перерандексированное семейство, построенное из f и применённое к typein i, равно f i.

LaTeX

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

Lean4

@[simp]
theorem bfamilyOfFamily_typein {ι} (f : ι → α) (i) : bfamilyOfFamily f (typein _ i) (typein_lt_type _ i) = f i :=
  bfamilyOfFamily'_typein _ f i

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