finTwoArrow — Mathlib

English

There is a uniform isomorphism between α^2 and α × α given by evaluating at the two coordinates.

Русский

Существует равномерный изоморфизм между α^2 и α × α, задаваемый парой координат.

LaTeX

$$$(\\mathrm{Fin}(2) \\to α) \\cong_{u} α \\times α$$$

Lean4

/-- Uniform isomorphism between `α² = Fin 2 → α` and `α × α`. -/
@[simps! -fullyApplied]
def finTwoArrow (α : Type*) [UniformSpace α] : (Fin 2 → α) ≃ᵤ α × α :=
  { piFinTwo fun _ => α with toEquiv := finTwoArrowEquiv α }

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