symm_trans — Mathlib

English

The symmetric (reversed) version of a glued relative homotopy satisfies the relation (F trans G).symm = G.symm trans F.symm.

Русский

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

LaTeX

$$$(F\trans G)^{\mathrm{symm}} = G^{\mathrm{symm}} \trans F^{\mathrm{symm}}$.$$

Lean4

theorem symm_trans (F : HomotopyRel f₀ f₁ S) (G : HomotopyRel f₁ f₂ S) : (F.trans G).symm = G.symm.trans F.symm :=
  HomotopyWith.ext <| Homotopy.congr_fun <| Homotopy.symm_trans _ _

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