instDFunLike — Mathlib

English

The evaluation map on the restricted product is the projection to the coordinate function, i.e., the restriction to the first component gives the canonical function from x to x.1 at each index.

Русский

Оценка на ограниченном произведении равна проекции на координату: отображение x ↦ x.1 на каждом индексе.

LaTeX

$$$\\mathrm{coe}(x,i) = x.1(i), \\quad \\text{with } x \\in \\mathrm{RestrictedProduct} \\text{ and } i\\in I.$$$

Lean4

instance : DFunLike (Πʳ i, [R i, A i]_[𝓕]) ι R where
  coe x i := x.1 i
  coe_injective' _ _ := Subtype.ext

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