English
Applying pi to a family fp at an argument c yields the i-th component fp i at c.
Русский
Применение pi к семейству fp в аргументе c даёт i-ую компоненту fp i в c.
LaTeX
$$$ pi \\; fp \\, c \\, i = fp i \\, c $$$
Lean4
/-- `pi` construction for affine maps. From a family of affine maps it produces an affine
map into a family of affine spaces.
This is the affine version of `LinearMap.pi`.
-/
@[simps linear]
def pi (f : (i : ι) → (P1 →ᵃ[k] φp i)) : P1 →ᵃ[k] ((i : ι) → φp i)
where
toFun m a := f a m
linear := LinearMap.pi (fun a ↦ (f a).linear)
map_vadd' _
_ :=
funext fun _ ↦
map_vadd _ _
_
--fp for when the image is a dependent AffineSpace φp i, fv for when the
--image is a Module φv i, f' for when the image isn't dependent.
