restrict — Mathlib

English

If p defines a perfect pairing on M,N, then its restriction to submodules via injective maps i and j yields a perfect pairing on the restricted submodules.

Русский

Если p задаёт совершенное парирование на M,N, то его ограничение на подмодули через инъекции i и j образуют совершенное парирование на ограниченных подпространствах.

LaTeX

$$(p|_{i,j}).IsPerfPair$$

Lean4

/-- The restriction of a perfect pairing to submodules is a perfect pairing. -/
theorem restrict : (p.compl₁₂ i j).IsPerfPair
    where
  bijective_left := p.restrict_aux i j hi hj hij
  bijective_right := p.flip.restrict_aux j i hj hi hij.flip

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