English
There is a uniform isomorphism between dependent functions Π i : Fin 2, α i and the product α0 × α1.
Русский
Существует равномерный изоморфизм между зависимыми функциями Π i : Fin 2, α_i и произведением α0 × α1.
LaTeX
$$$(\\forall i:\\mathrm{Fin}(2), \\alpha(i)) \\cong_{u} (\\alpha(0) \\times \\alpha(1))$$$
Lean4
/-- Uniform isomorphism between dependent functions `Π i : Fin 2, α i` and `α 0 × α 1`. -/
@[simps! -fullyApplied]
def piFinTwo (α : Fin 2 → Type u) [∀ i, UniformSpace (α i)] : (∀ i, α i) ≃ᵤ α 0 × α 1
where
toEquiv := piFinTwoEquiv α
uniformContinuous_toFun := (Pi.uniformContinuous_proj _ 0).prodMk (Pi.uniformContinuous_proj _ 1)
uniformContinuous_invFun :=
uniformContinuous_pi.mpr <| Fin.forall_fin_two.2 ⟨uniformContinuous_fst, uniformContinuous_snd⟩
