fromLoop_trans_toLoop — Mathlib

English

The fromLoop construction applied to the concatenation of two i-loops equals the concatenation operation transAt of the corresponding GenLoop elements.

Русский

Применение fromLoop к конкатенации двух i-петель равно конкатенации GenLoop элементов через transAt.

LaTeX

$$$\\mathrm{fromLoop}(i)(\\mathrm Path.trans(\\mathrm{toLoop}(i p), \\mathrm{toLoop}(i q))) = \\mathrm{transAt}(i,p,q)$$$

Lean4

theorem fromLoop_trans_toLoop {i : N} {p q : Ω^ N X x} :
    fromLoop i ((toLoop i p).trans <| toLoop i q) = transAt i p q :=
  (copy_eq _ _).symm

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