toPMap_domain — Mathlib

English

Let f be a linear map E → F over R and p a submodule of E. The partially defined map f.toPMap p has domain exactly p.

Русский

Пусть f: E → F линейное отображение над R и p — подмодуль E. Частично заданное отображение f.toPMap p имеет область определения, равную p.

LaTeX

$$$\operatorname{dom}(f|_p) = p$$$

Lean4

@[simp]
theorem toPMap_domain (f : E →ₗ[R] F) (p : Submodule R E) : (f.toPMap p).domain = p :=
  rfl

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