English
There is a natural equivalence between the two ways of associating a triple product: ((α × β) × γ) and α × (β × γ); concretely, ((a,b),c) corresponds to (a,b,c) and conversely.
Русский
Существует естественная эквивалентность между двумя скобочными вариантами тройного произведения: ((α × β) × γ) и α × (β × γ); явно, ((a,b),c) соответствует (a,b,c) и обратно.
LaTeX
$$$$ ((a,b),c) \\quad\\longleftrightarrow\\quad (a,b,c). $$$$
Lean4
/-- Type product is associative up to an equivalence. -/
@[simps (attr := grind =)]
def prodAssoc (α β γ) : (α × β) × γ ≃ α × β × γ :=
⟨fun p => (p.1.1, p.1.2, p.2), fun p => ((p.1, p.2.1), p.2.2), fun ⟨⟨_, _⟩, _⟩ => rfl, fun ⟨_, ⟨_, _⟩⟩ => rfl⟩
