measurableEquivPi — Mathlib

English

There exists a measurable equivalence between the complex field ℂ and the real 2-dimensional space ℝ^2.

Русский

Существует измеримая эквивалентность между комплексами ℂ и плоскостью ℝ^2.

LaTeX

$$$\mathbb{C} \ \equiv_{\text{meas}} \mathbb{R}^2$$$

Lean4

/-- Measurable equivalence between `ℂ` and `ℝ² = Fin 2 → ℝ`. -/
def measurableEquivPi : ℂ ≃ᵐ (Fin 2 → ℝ) :=
  basisOneI.equivFun.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv

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