English
The composition of two LinearPMaps f and g is a new LinearPMap from E to G with domain dom(f) and value g f on that domain, assuming the compatibility condition holds.
Русский
Композиция двух частично заданных линейных отображений f и g образует новое частично заданное отображение E → G с доменом dom(f) и значением g(f(x)) на этом домене, при условии совместимости.
LaTeX
$$$\text{comp}(g,f,H) : E \to\cdot G$, with $\operatorname{dom}(\text{comp}(g,f,H)) = \operatorname{dom}(f)$ and $(\text{comp}(g,f,H))(x) = g(f(x))$ for $x \in \operatorname{dom}(f)$.$$
Lean4
/-- The tuple `(x, f x)` is contained in the graph of `f`. -/
theorem mem_graph (f : E →ₗ.[R] F) (x : domain f) : ((x : E), f x) ∈ f.graph := by simp
