re_apply_eq_re — Mathlib

English

If a linear isometry f satisfies f 1 = 1, then (f z).re = z.re for all z.

Русский

Если f — линейная изометрия и f 1 = 1, то для любого z имеет место (f z).re = z.re.

LaTeX

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

Lean4

theorem re_apply_eq_re {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : (f z).re = z.re :=
  by
  apply LinearIsometry.re_apply_eq_re_of_add_conj_eq
  intro z
  apply LinearIsometry.im_apply_eq_im h

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