norm_le_abs_re_add_abs_im

Mathlib.Analysis.Complex.Norm

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

English

For any z, the norm is bounded by the sum of absolute values of its real and imaginary parts: ||z|| ≤ |Re z| + |Im z|.

Русский

Для любого z выполняется неравенство: ||z|| ≤ |Re z| + |Im z|.

LaTeX

$$$\\forall z \\in \\mathbb{C}, \\|z\\| \\le |\\Re z| + |\\Im z|$$$

Lean4

theorem norm_le_abs_re_add_abs_im (z : ℂ) : ‖z‖ ≤ |z.re| + |z.im| := by
  simpa [re_add_im] using norm_add_le (z.re : ℂ) (z.im * I)

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

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

Разделы

Аффилиация

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