continuous_normSq — Mathlib

English

The squared modulus function z ↦ |z|^2 is continuous on ℂ; equivalently, norm squared is a continuous map from ℂ to ℝ.

Русский

Функция z ↦ |z|^2 непрерывна на ℂ; то есть квадрат нормы является непрерывной отображением из ℂ в ℝ.

LaTeX

$$$ \\text{Continuous } (z \\mapsto |z|^{2}) $$$

Lean4

@[continuity, fun_prop]
theorem continuous_normSq : Continuous normSq := by
  simpa [← Complex.normSq_eq_norm_sq] using continuous_norm (E := ℂ).pow 2

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