norm_sub_one_sq_eqOn_sphere — Mathlib

English

On the sphere of radius 1 around 0, the same relation holds: ‖z−1‖^2 = 2(1 − Re z) for ‖z‖ = 1.

Русский

На сфере радиуса 1 вокруг 0 выполняется аналогичное равенство: ‖z−1‖^2 = 2(1 − Re z) при ‖z‖ = 1.

LaTeX

$$$\\|z-1\\|^2 = 2\\,(1-\\Re z) \\quad\\text{when } \\|z\\| = 1$$$

Lean4

theorem norm_sub_one_sq_eqOn_sphere : (Metric.sphere (0 : ℂ) 1).EqOn (‖· - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) :=
  fun z hz ↦ norm_sub_one_sq_eq_of_norm_one (by simpa using hz)

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