symm_trans — Mathlib

English

The symmetrical of a concatenation of homotopies satisfies the relation: (F.trans G).symm = G.symm.trans F.symm.

Русский

Симметрическая часть конкатенации гомотопий удовлетворяет: (F.trans G).symm = G.symm.trans F.symm.

LaTeX

$$$\forall F : p_0.Homotopy p_1,\; G : p_1.Homotopy p_2,\; (F.trans G).symm = G.symm.trans F.symm$$$

Lean4

theorem symm_trans (F : Homotopy p₀ p₁) (G : Homotopy p₁ p₂) : (F.trans G).symm = G.symm.trans F.symm :=
  ContinuousMap.HomotopyRel.symm_trans _ _

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