im_apply_eq_im_or_neg_of_re_apply_eq_re

English

If a linear isometry f preserves the real part, then for any z, (f z).im is either z.im or - z.im.

Русский

Если линейная изометрия сохраняет вещественную часть, то для любого z мнимая часть либо сохраняется, либо меняется на противоположную.

LaTeX

$$$\forall {f : ℂ \toℓᵢ[ℝ] ℂ}, (\forall z, (f z).re = z.re) \rightarrow \forall z, (f z).im = z.im \lor (f z).im = -z.im$$$

Lean4

theorem im_apply_eq_im_or_neg_of_re_apply_eq_re {f : ℂ →ₗᵢ[ℝ] ℂ} (h₂ : ∀ z, (f z).re = z.re) (z : ℂ) :
    (f z).im = z.im ∨ (f z).im = -z.im := by
  have h₁ := f.norm_map z
  simp only [norm_def] at h₁
  rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z, h₂, add_left_cancel_iff,
    mul_self_eq_mul_self_iff] at h₁

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