re_le_neg_norm_iff_eq_neg_norm — Mathlib

English

The real part is bounded above by the negative norm exactly when z equals minus its norm.

Русский

Действительная часть ограничена сверху противомеры минуса нормы тогда и только тогда, когда z равно минус своей нормы.

LaTeX

$$$ \operatorname{re}(z) \le -\|z\| \iff z = -\|z\| $$$

Lean4

theorem re_le_neg_norm_iff_eq_neg_norm {z : K} : re z ≤ -‖z‖ ↔ z = -‖z‖ := by
  simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_re_iff_eq_norm (z := -z)

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