transAt_indep — Mathlib

English

The value of transAt i f g in the homotopy quotient is independent of the index i.

Русский

Значение transAt i f g в фактор-группе гомотопий не зависит от i.

LaTeX

$$$\\langle \\mathrm{transAt}\\ i\\ f\\ g\\rangle = \\langle \\mathrm{transAt}\\ j\\ f\\ g\\rangle$ in HomotopyGroup$$

Lean4

theorem transAt_indep {i} (j) (f g : Ω^ N X x) : (⟦transAt i f g⟧ : HomotopyGroup N X x) = ⟦transAt j f g⟧ :=
  by
  simp_rw [← fromLoop_trans_toLoop]
  let m := fun (G) (_ : Group G) => ((· * ·) : G → G → G)
  exact congr_fun₂ (congr_arg (m <| HomotopyGroup N X x) <| auxGroup_indep i j) ⟦g⟧ ⟦f⟧

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