Theorems · Theorem · algebraic topology

GenLoop.transAt_distrib

∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] {i j : N},
  i ≠ j →
    ∀ (a b c d : ↑(GenLoop N X x)),
      GenLoop.transAt i (GenLoop.transAt j a b) (GenLoop.transAt j c d) =
        GenLoop.transAt j (GenLoop.transAt i a c) (GenLoop.transAt i b d)

Defined in

Mathlib.Topology.Homotopy.HomotopyGroup

Cited by

1 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceDecidableEq