finTwoArrow — Mathlib

English

There is a natural continuous linear equivalence between the space of functions from Fin 2 to M and the product M × M, given by assembling the two coordinates into a pair.

Русский

Существует естественное непрерывно-линейное эквивалентное отображение между пространством функций Fin 2 → M и произведением M × M, собирающее две координаты в пару.

LaTeX

$$$ (\\mathrm{FinTwoArrow}\\; R\; M) : (\\mathrm{Fin}\\; 2 \\to M) \\cong_L[R] M \\times M, \\quad (g \\mapsto (g(0), g(1))) $$$

Lean4

/-- Continuous linear equivalence between vectors in `M² = Fin 2 → M` and `M × M`. -/
@[simps! -fullyApplied apply symm_apply]
def finTwoArrow : (Fin 2 → M) ≃L[R] M × M :=
  { piFinTwo R fun _ => M with toLinearEquiv := LinearEquiv.finTwoArrow R M }

Похожие утверждения