English
Restrict the codomain of a LinearPMap f to a submodule p of F, provided that f(x) ∈ p for all x in dom(f). The resulting map has the same domain as f and codomain p.
Русский
Ограничиваем кодом отображение LinearPMap f до подмодуля p ⊆ F, если для всех x в dom(f) выполнено f(x) ∈ p. Полученное отображение имеет ту же область определения, что и f, но кодом является p.
LaTeX
$$$\operatorname{dom}(\mathrm{codRestrict}(f,p)) = \operatorname{dom}(f) \quad\text{and}\quad \mathrm{codRestrict}(f,p) : E \to p$$$
Lean4
/-- Restrict codomain of a `LinearPMap` -/
def codRestrict (f : E →ₗ.[R] F) (p : Submodule R F) (H : ∀ x, f x ∈ p) : E →ₗ.[R] p
where
domain := f.domain
toFun := f.toFun.codRestrict p H
