measurableEquivRealProd

Mathlib.MeasureTheory.Measure.Lebesgue.Complex

URI: https://scilib.ai/kg/mathlib#Complex.measurableEquivRealProd

English

There is a measurable equivalence between ℂ and ℝ × ℝ.

Русский

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

LaTeX

$$$\mathbb{C} \equiv_{\text{meas}} \mathbb{R} \times \mathbb{R}$$$

Lean4

/-- Measurable equivalence between `ℂ` and `ℝ × ℝ`. -/
def measurableEquivRealProd : ℂ ≃ᵐ ℝ × ℝ :=
  equivRealProdCLM.toHomeomorph.toMeasurableEquiv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru