English
If F: f0 ~ f1 and G: f1 ~ f2 are Homotopies, then the inverse of their concatenation equals the concatenation of their inverses in reverse order: (F.trans G).symm = G.symm.trans F.symm.
Русский
Если F: f0 ~ f1 и G: f1 ~ f2 — гомотопии, то обратная к их конкатенации равна конкатенации их обратных в обратном порядке: (F.trans G).symm = G.symm.trans F.symm.
LaTeX
$$$$(F \text{ trans } G)^{-1} = G^{-1} \text{ trans } F^{-1}$$$$
Lean4
theorem symm_trans {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) :
(F.trans G).symm = G.symm.trans F.symm := by
ext ⟨t, _⟩
rw [trans_apply, symm_apply, trans_apply]
simp only [coe_symm_eq, symm_apply]
split_ifs with h₁ h₂ h₂
· have ht : (t : ℝ) = 1 / 2 := by linarith
norm_num [ht]
· congr 2
apply Subtype.ext
simp only [coe_symm_eq]
linarith
· congr 2
apply Subtype.ext
simp only [coe_symm_eq]
linarith
· exfalso
linarith
