domRestrict — Mathlib

English

Restrict a partially defined map f to a submodule S of E contained in f.domain; the result has domain S ∩ f.domain and the same action on that set.

Русский

Ограничиваем частично заданное отображение f до подмодуля S ⊆ E, содержащегося в dom(f); полученное отображение имеет домен S ∩ dom(f) и действует там же.

LaTeX

$$$\mathrm{domRestrict}(f,S)\;:\; E \to\cdot F\quad\text{has domain } S \cap \operatorname{dom}(f)$$$

Lean4

/-- Restrict a partially defined linear map to a submodule of `E` contained in `f.domain`. -/
def domRestrict (f : E →ₗ.[R] F) (S : Submodule R E) : E →ₗ.[R] F :=
  ⟨S ⊓ f.domain, f.toFun.comp (Submodule.inclusion (by simp))⟩

Похожие утверждения