English
There exists a canonical uniform isomorphism between ((α × β) × γ) and α × (β × γ) given by the standard associator; all the structure maps are uniformly continuous.
Русский
Существует каноническое равномерное изоморФМ между ((α × β) × γ) и α × (β × γ), заданное обычной ассоциативной перестановкой; все отображения, вовлечённые в структуру, равномерно непрерывны.
LaTeX
$$$((\\alpha \\times \\beta) \\times \\gamma) \\cong_{u} \\alpha \\times (\\beta \\times \\gamma)$$$
Lean4
/-- `(α × β) × γ` is uniformly isomorphic to `α × (β × γ)`. -/
def prodAssoc : (α × β) × γ ≃ᵤ α × β × γ
where
uniformContinuous_toFun :=
(uniformContinuous_fst.comp uniformContinuous_fst).prodMk
((uniformContinuous_snd.comp uniformContinuous_fst).prodMk uniformContinuous_snd)
uniformContinuous_invFun :=
(uniformContinuous_fst.prodMk (uniformContinuous_fst.comp uniformContinuous_snd)).prodMk
(uniformContinuous_snd.comp uniformContinuous_snd)
toEquiv := Equiv.prodAssoc α β γ
