English
The graph of f.coprod g projected to the E-coordinate yields the domain f.domain, and to the F-coordinate yields g.domain.
Русский
Граф f.coprod g проецируется на координату E в dom(f) и на координату F в dom(g).
LaTeX
$$$\text{graph}(f\mathrm{ coprod } g) \xrightarrow{\text{fst}} \operatorname{dom}(f), \quad \text{graph}(f\mathrm{ coprod } g) \xrightarrow{\text{snd}} \operatorname{dom}(g).$$$
Lean4
theorem graph_map_fst_eq_domain (f : E →ₗ.[R] F) : f.graph.map (LinearMap.fst R E F) = f.domain :=
by
ext x
simp only [Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, LinearMap.fst_apply,
Prod.exists, exists_and_right, exists_eq_right]
constructor <;> intro h
· rcases h with ⟨x, hx, _⟩
exact hx
· use f ⟨x, h⟩
simp only [h, exists_const]
