toLinearPMap_range — Mathlib

English

The range of the constructed LinearPMap equals the projection of the graph onto the second coordinate.

Русский

Образ построенного LinearPMap равен проекции графа на вторую координату.

LaTeX

$$\\mathrm{range}(g.toLinearPMap) = g.map(\\mathrm{snd})$$

Lean4

theorem toLinearPMap_range (g : Submodule R (E × F)) (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
    LinearMap.range g.toLinearPMap.toFun = g.map (LinearMap.snd R E F) := by
  rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]

Похожие утверждения