re_eq_norm — Mathlib

English

For every z ∈ ℂ, z.re = ||z|| if and only if 0 ≤ z in the complex order.

Русский

Для каждого z ∈ ℂ z.re = ||z|| тогда и только тогда, когда z ∈ ℂ положительно упорядочен (0 ≤ z).

LaTeX

$$$z.re = \|z\| \iff 0 \le z$$$

Lean4

@[simp]
theorem re_eq_norm {z : ℂ} : z.re = ‖z‖ ↔ 0 ≤ z :=
  have : 0 ≤ ‖z‖ := norm_nonneg z
  ⟨fun h ↦ ⟨h.symm ▸ this, (abs_re_eq_norm.1 <| h.symm ▸ abs_of_nonneg this).symm⟩, fun ⟨h₁, h₂⟩ ↦ by
    rw [← abs_re_eq_norm.2 h₂.symm, abs_of_nonneg h₁]⟩

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