proj_pi — Mathlib

English

Let fp be a family fp : ι → (P1 →ᵃ[k] φp i) of affine maps. Then the ith coordinate of the product map π fp is fp i; equivalently, for every i we have (proj i) ∘ (π fp) = fp i.

Русский

Пусть fp : ι → (P1 →ᵃ[k] φp i) задаёт семейство аффинных отображений. Тогда i-ая компонента произведения π fp равна fp i; более формально, для каждого i выполняется (proj i) ∘ (π fp) = fp i.

LaTeX

$$$\\forall i,\\ (\\operatorname{proj}_i) \\circ (\\pi fp) = fp i$$$

Lean4

theorem proj_pi (i : ι) : (proj i).comp (pi fp) = fp i :=
  ext fun _ => rfl

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