finTwoArrow — Mathlib

English

The space (Fin 2 → α) is measurably equivalent to α × α, via the coordinate map.

Русский

Пространство (Fin 2 → α) измеримо эквивалентно α × α через координатное отображение.

LaTeX

$$$ (\\mathrm{Fin}(2) \\to \\alpha) \\simeq^m \\alpha \\times \\alpha $$$

Lean4

/-- The space `Fin 2 → α` is measurably equivalent to `α × α`. -/
@[simps! -fullyApplied]
def finTwoArrow : (Fin 2 → α) ≃ᵐ α × α :=
  piFinTwo fun _ => α

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