isUniformEmbedding_equivRealProd — Mathlib

English

The natural uniform embedding of the complex plane into R^2 given by z ↦ (Re z, Im z).

Русский

Естественное равномерное вложение плоскости комплексных чисел в ℝ^2, задаваемое z ↦ (Re z, Im z).

LaTeX

$$$$ \\mathrm{IsUniformEmbedding}(\\operatorname{equivRealProd}). $$$$

Lean4

theorem isUniformEmbedding_equivRealProd : IsUniformEmbedding equivRealProd :=
  antilipschitz_equivRealProd.isUniformEmbedding lipschitz_equivRealProd.uniformContinuous

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