English
There is an auxiliary linear map from the projection g.map fst to F given by the rule x ↦ valFromGraph hg x.2, built from the graph g.
Русский
Существуют вспомогательные конструции линейного отображения от проекции g.map fst в F по правилу x ↦ valFromGraph hg x.2, построенные из графа g.
LaTeX
$$toLinearPMapAux : (g : Submodule R (E × F)) → (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) → g.map (fst) →ₗ[R] F$$
Lean4
/-- Define a `LinearMap` from its graph.
Helper definition for `LinearPMap`. -/
noncomputable def toLinearPMapAux (g : Submodule R (E × F))
(hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) : g.map (LinearMap.fst R E F) →ₗ[R] F
where
toFun := fun x => valFromGraph hg x.2
map_add' := fun v w => by
have hadd := (g.map (LinearMap.fst R E F)).add_mem v.2 w.2
have hvw := valFromGraph_mem hg hadd
have hvw' := g.add_mem (valFromGraph_mem hg v.2) (valFromGraph_mem hg w.2)
rw [Prod.mk_add_mk] at hvw'
exact (existsUnique_from_graph (@hg) hadd).unique hvw hvw'
map_smul' := fun a v => by
have hsmul := (g.map (LinearMap.fst R E F)).smul_mem a v.2
have hav := valFromGraph_mem hg hsmul
have hav' := g.smul_mem a (valFromGraph_mem hg v.2)
rw [Prod.smul_mk] at hav'
exact (existsUnique_from_graph (@hg) hsmul).unique hav hav'
