normSq_ofReal_sub_I_mul_sqrt_one_sub

English

If x is real with ‖x‖ ≤ 1, then ‖x − i√(1−x^2)‖^2 = 1, mirroring the previous identity with a minus.

Русский

Если x вещественно и ‖x‖ ≤ 1, то ‖x − i√(1−x^2)‖^2 = 1.

LaTeX

$$$\\|x - i\\sqrt{1 - x^2}\\|^2 = 1\\quad (|x| \\le 1)$$$

Lean4

theorem normSq_ofReal_sub_I_mul_sqrt_one_sub {x : ℝ} (hx : ‖x‖ ≤ 1) : normSq (x - I * √(1 - x ^ 2)) = 1 :=
  by
  rw [← normSq_neg, neg_sub', sub_neg_eq_add]
  simpa using normSq_ofReal_add_I_mul_sqrt_one_sub (x := -x) (by simpa)

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