domRestrict₁₂ — Mathlib

English

Applying the restricted map to x ∈ M and y ∈ q returns the same as applying f to x and then restricting to q.

Русский

Применение ограниченной карты к x и y в q равно применению f к x и последующему ограничению к q.

LaTeX

$$$ (f.domRestrict₂ q)(x)(y) = f(x)(y) $$$

Lean4

/-- Restricting a bilinear map in both components -/
def domRestrict₁₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) : p →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P :=
  (f.domRestrict p).domRestrict₂ q

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