norm_le_re_iff_eq_norm — Mathlib

English

For every z in K, the inequality ‖z‖ ≤ Re(z) holds exactly when z equals its norm.

Русский

Для каждого z в K неравенство ‖z‖ ≤ Re(z) выполняется тогда и только тогда, когда z равно своей норме.

LaTeX

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

Lean4

theorem norm_le_re_iff_eq_norm {z : K} : ‖z‖ ≤ re z ↔ z = ‖z‖ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have h' : ‖z‖ = re z := (le_antisymm (re_le_norm z) h).symm
    rw [h', re_eq_self_of_le h]
  · rw [h]
    simp

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