English
The domain of f restricted to S is S ∩ dom(f).
Русский
Область определения f, ограниченного до S, равна S ∩ dom(f).
LaTeX
$$$\operatorname{dom}(f|_S) = S \cap \operatorname{dom}(f).$$$
Lean4
/-- The graph of `-f` as a pushforward. -/
theorem neg_graph (f : E →ₗ.[R] F) :
(-f).graph = f.graph.map ((LinearMap.id : E →ₗ[R] E).prodMap (-(LinearMap.id : F →ₗ[R] F))) :=
by
ext ⟨x_fst, x_snd⟩
constructor <;> intro h
· rw [mem_graph_iff] at h
rcases h with ⟨y, hy, h⟩
rw [LinearPMap.neg_apply] at h
rw [Submodule.mem_map]
simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.neg_apply, Prod.mk_inj,
Prod.exists, exists_exists_and_eq_and]
use x_fst, y, hy
rw [Submodule.mem_map] at h
rcases h with ⟨x', hx', h⟩
cases x'
simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.neg_apply, Prod.mk_inj] at h
rw [mem_graph_iff] at hx' ⊢
rcases hx' with ⟨y, hy, hx'⟩
use y
rw [← h.1, ← h.2]
simp [hy, hx']
