guitartExact_of_isLeftDerivabilityStructure

English

If Φ.IsLeftDerivabilityStructure, then TwoSquare.GuitartExact ((Φ.catCommSq L₁ L₂).iso).inv holds.

Русский

Если Φ.IsLeftDerivabilityStructure, то TwoSquare.GuitartExact ((Φ.catCommSq L₁ L₂).iso).inv выполняется.

LaTeX

$$$[\Phi.IsLeftDerivabilityStructure] \Rightarrow TwoSquare.GuitartExact\big((\Phi.catCommSq L_1 L_2).iso\big).inv$$$

Lean4

theorem guitartExact_of_isLeftDerivabilityStructure [Φ.IsLeftDerivabilityStructure] :
    TwoSquare.GuitartExact ((Φ.catCommSq L₁ L₂).iso).inv :=
  guitartExact_of_isLeftDerivabilityStructure' _ _ _ _ _

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