English
The equality of graphs is proven by examining membership and applying the previous lemmas about valFromGraph and mem_graph_toLinearPMap.
Русский
Равенство графиков доказывается через разбор принадлежности и применения предыдущих лемм о valFromGraph и mem_graph_toLinearPMap.
LaTeX
$$toLinearPMap.graph = g ⇔ ... (proof sketch)$$
Lean4
@[simp]
theorem toLinearPMap_graph_eq (g : Submodule R (E × F))
(hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) : g.toLinearPMap.graph = g :=
by
ext ⟨x_fst, x_snd⟩
constructor <;> intro hx
· rw [LinearPMap.mem_graph_iff] at hx
rcases hx with ⟨y, hx1, hx2⟩
convert g.mem_graph_toLinearPMap hg y using 1
exact Prod.ext hx1.symm hx2.symm
rw [LinearPMap.mem_graph_iff]
have hx_fst : x_fst ∈ g.map (LinearMap.fst R E F) :=
by
simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
exact ⟨x_snd, hx⟩
refine ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩
rw [toLinearPMap_apply_aux hg]
exact (existsUnique_from_graph (@hg) hx_fst).unique (valFromGraph_mem hg hx_fst) hx
