English
This extensionality form states that if for every i the precomposition with the coordinate map from φv i to the product agrees, then the affine maps themselves are equal.
Русский
Эта форма экстенсиональности утверждает, что если для каждого i композиции с координатной картой дают равные отображения, то сами аффинные отображения равны.
LaTeX
$$$\big(\forall i,\ f\circ (\mathrm{single}\, _ i) = g\circ (\mathrm{single}\, _ i)\big) \Rightarrow f = g$$$
Lean4
/-- This is used as the ext lemma instead of `AffineMap.pi_ext_nonempty` for reasons explained in
note [partially-applied ext lemmas]. Analogous to `LinearMap.pi_ext'` -/
@[ext (iff := false)]
theorem pi_ext_nonempty' [Nonempty ι]
(h : ∀ i, f.comp (LinearMap.single _ _ i).toAffineMap = g.comp (LinearMap.single _ _ i).toAffineMap) : f = g :=
by
refine pi_ext_nonempty fun i x => ?_
convert AffineMap.congr_fun (h i) x
