mappingConeCompHomotopyEquiv_hom_inv_id

English

The homotopy equivalence between mappingCone g and mappingCone (mappingConeCompTriangle f g).mor1 has the property that the composition of its forward and inverse maps is the identity on mappingCone g.

Русский

Гомотопическая эквивалентность между mappingCone g и mappingCone (mappingConeCompTriangle f g).mor1 обладает свойством: композиция перехода вперёд и обратно равна тождественному отображению на mappingCone g.

LaTeX

$$$\text{hom}(f,g) \circ \text{inv}(f,g) = \mathrm{Id}$$$

Lean4

@[reassoc (attr := simp)]
theorem mappingConeCompHomotopyEquiv_hom_inv_id :
    (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv = 𝟙 _ := by
  simp [mappingConeCompHomotopyEquiv]

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