familyOfElements_apply — Mathlib

English

The section constructed from a compatible family evaluates to the corresponding elements on each Y_i.

Русский

Раздел, полученный от совместимой семьи элементов, при применении к каждому Y_i совпадает с данными элементами.

LaTeX

$$$\\forall i,\\ (\\mathrm{section_}(hY,hF).1)(\,\\mathrm{op}(Y_i)) = x_i$$$

Lean4

theorem familyOfElements_apply (hx : x.IsCompatible) {X Z : C} (f : Z ⟶ X) (i : I) (φ : Z ⟶ Y i) :
    familyOfElements x X f ⟨i, ⟨φ⟩⟩ = F.map φ.op (x i) := by apply hx

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