rootSpan_dualAnnihilator_le_ker_rootForm

English

The image of the dual annihilator of the root span under flip-to-perf-pair is contained in the kernel of CorootForm.

Русский

Образ двойственного аннигиллятора корневого охвата под отображением flip_to_perf_pair содержится в ядре CorootForm.

LaTeX

$$$(P.rootSpan\\ R).dualAnnihilator.map P.flip.toPerfPair.symm \\le \\ker P.CorootForm$$

Lean4

theorem rootSpan_dualAnnihilator_le_ker_rootForm :
    (P.rootSpan R).dualAnnihilator.map P.flip.toPerfPair.symm ≤ LinearMap.ker P.CorootForm :=
  P.flip.corootSpan_dualAnnihilator_le_ker_rootForm

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