English
Restrict a partially defined map to a submodule of E contained in its domain; the result is a new LinearPMap with domain S ∩ dom(f) and same action on that domain.
Русский
Ограничиваем частично заданное отображение до подмодуля S ⊆ E, содержащегося в dom(f); результат — новое LinearPMap с доменом S ∩ dom(f) и тем же действием на этом домене.
LaTeX
$$$f|_S : E \to\cdot F \quad\text{has domain } S \cap \operatorname{dom}(f).$$$
Lean4
/-- The graph of `z • f` as a pushforward. -/
theorem smul_graph (f : E →ₗ.[R] F) (z : M) :
(z • f).graph = f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (z • (LinearMap.id : F →ₗ[R] F))) :=
by
ext ⟨x_fst, x_snd⟩
constructor <;> intro h
· rw [mem_graph_iff] at h
rcases h with ⟨y, hy, h⟩
rw [LinearPMap.smul_apply] at h
rw [Submodule.mem_map]
simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.smul_apply, Prod.mk_inj,
Prod.exists, exists_exists_and_eq_and]
use x_fst, y, hy
rw [Submodule.mem_map] at h
rcases h with ⟨x', hx', h⟩
cases x'
simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.smul_apply, Prod.mk_inj] at h
rw [mem_graph_iff] at hx' ⊢
rcases hx' with ⟨y, hy, hx'⟩
use y
rw [← h.1, ← h.2]
simp [hy, hx']
