re_extendTo𝕜'ₗ — Mathlib

English

For any g in StrongDual ℝ E, the real part of its extension equals g on E; i.e., re(extendTo𝕜'ℓ g x) = g x for all x.

Русский

Для любого g в StrongDual ℝ E, вещественная часть его продолжения равна g на E: re(extendTo𝕜'ℓ g x) = g x для всех x.

LaTeX

$$$\mathrm{re}((\mathrm{extendTo𝕜'ℓ} g)(x)) = g(x)$$$

Lean4

@[simp]
theorem re_extendTo𝕜'ₗ [ContinuousConstSMul 𝕜 E] (g : StrongDual ℝ E) (x : E) : re ((extendTo𝕜'ₗ g) x : 𝕜) = g x :=
  by
  have h g (x : E) : extendTo𝕜'ₗ g x = ((g x : 𝕜) - (I : 𝕜) * (g ((I : 𝕜) • x) : 𝕜)) := rfl
  simp only [h, map_sub, ofReal_re, mul_re, I_re, zero_mul, ofReal_im, mul_zero, sub_self, sub_zero]

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