cfcₙHom_real_eq_restrict — Mathlib

English

The map cfcₙHom equals the real-restricted version of cfcHom restricted to the spectrum.

Русский

Отображение cfcₙHom равно вещественно ограниченной версии cfcHom, ограниченной спектром.

LaTeX

$$$$ cfcₙHom ha = \\text{SpectrumRestricts}(cfcₙHom, a) $$$$

Lean4

theorem cfcₙHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) :
    cfcₙHom ha =
      ha.quasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ha.isStarNormal) (R := ℝ) (S := ℂ) (f := Complex.reCLM) :=
  ha.quasispectrumRestricts.cfcₙHom_eq_restrict _ Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal

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