re_le_norm

Mathlib.Analysis.Complex.Norm

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

English

For every z ∈ ℂ, the real part is bounded above by the norm: Re(z) ≤ ‖z‖.

Русский

Для каждого z ∈ ℂ действительная часть числа не превосходит модуль: Re(z) ≤ ‖z‖.

LaTeX

$$$\forall z \in \mathbb{C},\; \Re(z) \le \|z\|$$$

Lean4

theorem re_le_norm (z : ℂ) : z.re ≤ ‖z‖ :=
  (abs_le.1 (abs_re_le_norm _)).2

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

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

Разделы

Аффилиация

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