cfcₙHom_nnreal_eq_restrict — Mathlib

English

For a ≥ 0, cfcₙHom ha equals the nnreal-restricted nonunital star algebra hom.

Русский

Для a ≥ 0, cfcₙHom ha равен nnreal-ограниченному ненулевому звездному отображению.

LaTeX

$$$$ cfcₙHom ha = (QuasispectrumRestricts.nnreal_of_nonneg ha).nonUnitalStarAlgHom (cfcₙHom (IsSelfAdjoint.of_nonneg ha)) $$$$

Lean4

theorem cfcₙHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) :
    cfcₙHom ha =
      (QuasispectrumRestricts.nnreal_of_nonneg ha).nonUnitalStarAlgHom (cfcₙHom (IsSelfAdjoint.of_nonneg ha)) :=
  by apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict _ isUniformEmbedding_subtype_val

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