English
Twice-distributivity of concatenation along coordinates holds for i ≠ j.
Русский
Двойное распределение конкатенации по координатам действительно при i ≠ j.
LaTeX
$$$transAt_i (transAt_j a b) (transAt_j c d) = transAt_j (transAt_i a c) (transAt_i b d)$, при i ≠ j$$
Lean4
/-- The homotopy "group" indexed by an empty type is in bijection with
the path components of `X`, aka the `ZerothHomotopy`. -/
def homotopyGroupEquivZerothHomotopyOfIsEmpty (N x) [IsEmpty N] : HomotopyGroup N X x ≃ ZerothHomotopy X :=
Quotient.congr (genLoopHomeoOfIsEmpty N x).toEquiv
(by
-- joined iff homotopic
intro a₁ a₂
constructor <;> rintro ⟨H⟩
exacts
[⟨{ toFun := fun t => H ⟨t, isEmptyElim⟩
source' := (H.apply_zero _).trans (congr_arg a₁ <| Subsingleton.elim _ _)
target' := (H.apply_one _).trans (congr_arg a₂ <| Subsingleton.elim _ _) }⟩,
⟨{ toFun := fun t0 => H t0.fst
map_zero_left := fun _ => H.source.trans (congr_arg a₁ <| Subsingleton.elim _ _)
map_one_left := fun _ => H.target.trans (congr_arg a₂ <| Subsingleton.elim _ _)
prop' := fun _ _ ⟨i, _⟩ => isEmptyElim i }⟩])
