toLinearPMap_apply_aux — Mathlib

English

The domain of the constructed LinearPMap equals the projection g.map fst.

Русский

Область определения построенного LinearPMap равна проекции g.map fst.

LaTeX

$$\\mathrm{domain}(g.toLinearPMap) = g.map(\\mathrm fst)$$

Lean4

theorem toLinearPMap_apply_aux {g : Submodule R (E × F)}
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) (x : g.map (LinearMap.fst R E F)) :
    g.toLinearPMap x = valFromGraph hg x.2 := by
  classical
  change (if hg : _ then g.toLinearPMapAux hg else 0) x = _
  rw [dif_pos]
  · rfl
  · exact hg

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