domRestrict₂_apply — Mathlib

English

Restricting a bilinear map in the second entry yields a bilinear map on a submodule q of N, defined by m ↦ (f m)|_q.

Русский

Ограничение билинейной карты во второй переменной даёт билинейную карту на подмодуле q в N, задаваемую m ↦ (f m)|_q.

LaTeX

$$$ (f.domRestrict₂ q) : M \\to q \\to P\\quad\\text{is bilinear and } (f.domRestrict₂ q)(m)(y) = f(m)(y) $ for y ∈ q.$$

Lean4

theorem domRestrict₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) (x : M) (y : q) :
    f.domRestrict₂ q x y = f x y :=
  rfl

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