English
If the index type ι is nonempty, two affine maps f,g : ((i → φv i) →ᵃ[k] P2) are equal whenever they agree on all Pi.single evaluations, i.e., f(Pi.single i x) = g(Pi.single i x) for all i and x.
Русский
Если множество индексов ι непусто, то две аффинные отображения f,g : ((i → φv i) →ᵃ[k] P2) равны, когда они совпадают на всех значениях Pi.single: f(Pi.single i x) = g(Pi.single i x) для всех i и x.
LaTeX
$$$\forall i\forall x\; f(\Pi.single i x) = g(\Pi.single i x) \Rightarrow f = g$ (при условии $ι$ непустого)$$
Lean4
/-- Two affine maps from a Pi-type of modules `(i : ι) → φv i` are equal if they are equal in their
operation on `Pi.single` and `ι` is nonempty. Analogous to `LinearMap.pi_ext`. See also
`pi_ext_zero`, which instead of `Nonempty ι` requires agreement at 0. -/
theorem pi_ext_nonempty [Nonempty ι] (h : ∀ i x, f (Pi.single i x) = g (Pi.single i x)) : f = g :=
by
apply pi_ext_zero h
inhabit ι
rw [← Pi.single_zero default]
apply h
