hasLeftHomology_of_preserves' — Mathlib

English

If S has left homology and F preserves the left homology of S, then the image F.mapShortComplex.obj S has left homology.

Русский

Если S обладает левой гомологией и F сохраняет левую гомологию S, то изображение F.mapShortComplex.obj S сохраняет левую гомологию.

LaTeX

$$$S\text{ HasLeftHomology} \wedge F\text{PreservesLeftHomologyOf S} \Rightarrow (F.mapShortComplex.obj S).HasLeftHomology.$$$

Lean4

instance hasLeftHomology_of_preserves' [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
    (F.mapShortComplex.obj S).HasLeftHomology := by dsimp; infer_instance

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