im_le_norm

Mathlib.Analysis.Complex.Norm

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

English

The imaginary part is at most the norm: Im(z) ≤ ||z|| (trivial since ||z|| ≥ 0).

Русский

Мнимая часть не превосходит норму: Im(z) ≤ ||z||.

LaTeX

$$$\\forall z \\in \\mathbb{C}, \\operatorname{Im}(z) \\le \\|z\\|$$$

Lean4

theorem im_le_norm (z : ℂ) : z.im ≤ ‖z‖ :=
  (abs_le.1 (abs_im_le_norm _)).2

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

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

Разделы

Аффилиация

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