range_domRestrict — Mathlib

English

Restricting the domain of a linear map f to a submodule K yields a map whose range is exactly K mapped under f: range(f.domRestrict K) = K.map f.

Русский

Ограничение области определения линейного отображения f до подмодуля K даёт образ, равный изображению K под действием f: range(f.domRestrict K) = K.map f.

LaTeX

$$$\operatorname{range}(f.\mathrm{domRestrict} K) = K.\operatorname{map} f$$$

Lean4

@[simp]
theorem range_domRestrict [Module R M₂] (K : Submodule R M) (f : M →ₗ[R] M₂) : range (domRestrict f K) = K.map f := by
  ext; simp

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