English
The left and right injections are isometries into the disjoint union with the glued distance; swapping the two components preserves the glueDist up to symmetry.
Русский
Левые и правые вложения являются изометриями в дискретное объединение с заданной дистанцией; важно, что перестановка компонентов сохраняет glueDist.
LaTeX
$$$ glueDist(\mathrm{Sum.inl}, \mathrm{Sum.inr},ε) \,=\, glueDist(\mathrm{Sum.inr}, \mathrm{Sum.inl},ε) \quad \text{up to swap}. $$$
Lean4
theorem glueDist_swap (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) : ∀ x y, glueDist Ψ Φ ε x.swap y.swap = glueDist Φ Ψ ε x y
| .inl _, .inl _ => rfl
| .inr _, .inr _ => rfl
| .inl _, .inr _ => by simp only [glueDist, Sum.swap_inl, Sum.swap_inr, add_comm]
| .inr _, .inl _ => by simp only [glueDist, Sum.swap_inl, Sum.swap_inr, add_comm]
