English
There is a continuous linear equivalence between the dependent function space (i ∈ Fin 2) → M i and the product M0 × M1, given by the coordinate-wise identification g ↦ (g(0), g(1)).
Русский
Существует непрерывно-линейное эквивалентное отображение между зависимым пространством функций (i ∈ Fin 2) → M i и произведением M0 × M1, задаваемое ассоциированием по координатам: g ↦ (g(0), g(1)).
LaTeX
$$$ ((i: Fin 2) \to M i) \cong_L[R] M_0 \times M_1, \quad (g \mapsto (g(0), g(1))) $$$
Lean4
/-- Continuous linear equivalence between dependent functions `(i : Fin 2) → M i` and `M 0 × M 1`.
-/
@[simps! -fullyApplied apply symm_apply]
def piFinTwo (M : Fin 2 → Type*) [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] [∀ i, TopologicalSpace (M i)] :
((i : _) → M i) ≃L[R] M 0 × M 1 :=
{ Homeomorph.piFinTwo M with toLinearEquiv := LinearEquiv.piFinTwo R M }
