restrict — Mathlib

English

Restricting the domain and codomain of a linear map to compatible submodules yields a linear map between subtypes.

Русский

Ограничение области и кодомодуля линейного отображения даёт линейное отображение между сопутствующими подмножествами.

LaTeX

$$$f.restrict : p \to q$ with hf$$

Lean4

/-- Restrict domain and codomain of a linear map. -/
def restrict (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ x ∈ p, f x ∈ q) : p →ₗ[R] q :=
  (f.domRestrict p).codRestrict q <| SetLike.forall.2 hf

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