English
Equivalent reformulation: equality of affine maps is equivalent to equality of linear parts and a pointwise equality at some point.
Русский
Эквивалентная формулировка: равенство аффинных отображений эквивалентно равенству линейных частей и существованию точки с равенством значений.
LaTeX
$$f = g ↔ (f.linear = g.linear) ∧ ∃ p, f p = g p$$
Lean4
/-- Two affine maps are equal if they have equal linear maps and are equal at some point. -/
theorem ext_linear {f g : P1 →ᵃ[k] P2} (h₁ : f.linear = g.linear) {p : P1} (h₂ : f p = g p) : f = g :=
by
ext q
have hgl : g.linear (q -ᵥ p) = toFun g ((q -ᵥ p) +ᵥ q) -ᵥ toFun g q := by simp
have := f.map_vadd' q (q -ᵥ p)
rw [h₁, hgl, toFun_eq_coe, map_vadd, linearMap_vsub, h₂] at this
simpa
