English
If V is a span of S, then two linear maps f,g: V→N are equal iff they agree on images of S.
Русский
Если V = span(S), то линейные отображения совпадают, если совпадают на образах элементов из S.
LaTeX
$$$f=g \iff \forall s\in S, f(s)=g(s)$, при условии $V=\operatorname{span} R S$.$$
Lean4
theorem linearMap_eq_iff_of_eq_span {V : Submodule R M} (f g : V →ₗ[R] N) {S : Set M} (hV : V = span R S) :
f = g ↔
∀ (s : S),
f ⟨s, by simpa only [hV] using subset_span (by simp)⟩ = g ⟨s, by simpa only [hV] using subset_span (by simp)⟩ :=
by
constructor
· rintro rfl _
rfl
· intro h
subst hV
suffices ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩
by
ext ⟨x, hx⟩
exact this x hx
intro x hx
induction hx using span_induction with
| mem x hx => exact h ⟨x, hx⟩
| zero => erw [map_zero, map_zero]
| add x y hx hy hx' hy' =>
erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
rw [hx', hy']
| smul a x hx hx' =>
erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
rw [hx']
