norm_sub_eq

Mathlib.Analysis.Complex.Arg

URI: https://scilib.ai/kg/mathlib#Complex.norm_sub_eq

English

If x.arg = y.arg, then ∥x − y∥ = ∥∥x∥ − ∥y∥∥.

Русский

Если x.arg = y.arg, то ∥x − y∥ = ∥∥x∥ − ∥y∥∥.

LaTeX

$$$$\|x - y\| = \bigl| \|x\| - \|y\| \bigr|.$$$$

Lean4

theorem norm_sub_eq (h : x.arg = y.arg) : ‖x - y‖ = ‖‖x‖ - ‖y‖‖ :=
  (sameRay_of_arg_eq h).norm_sub

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru