norm_sub_eq_iff — Mathlib

English

For complex numbers x,y, ∥x − y∥ = |∥x∥ − ∥y∥| if and only if x and y are on the same ray or one is zero.

Русский

Для комплексных чисел x,y: ∥x − y∥ = |∥x∥ − ∥y∥| тогда и только тогда, когда x,y лежат на одной луче или один из них равен нулю.

LaTeX

$$$$\|x - y\| = \bigl| \|x\| - \|y\| \bigr| \iff x=0 \lor y=0 \lor x.arg = y.arg.$$$$

Lean4

theorem norm_sub_eq_iff : ‖x - y‖ = |‖x‖ - ‖y‖| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
  sameRay_iff_norm_sub.symm.trans sameRay_iff

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