cfcₙHom_eq_restrict — Mathlib

English

As in the previous item, congruence of cfcₙHom under restriction holds; the restricted form equals the restricted form of the other predicate.

Русский

Как и в предыдущем пункте, сохраняется равенство под ограничением при конгруэнтности формул.

LaTeX

$$$Eq\\ (QuasispectrumRestricts.cfc\\nHom hpa)\\ (QuasispectrumRestricts.cfc\\nHom hqa)$$$

Lean4

theorem cfcₙHom_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a)
    (h : QuasispectrumRestricts a f) : cfcₙHom hpa = h.nonUnitalStarAlgHom (cfcₙHom hqa) :=
  by
  apply cfcₙHom_eq_of_continuous_of_map_id
  · exact h.isClosedEmbedding_nonUnitalStarAlgHom (cfcₙHom_isClosedEmbedding hqa) halg |>.continuous
  · exact h.nonUnitalStarAlgHom_id (cfcₙHom_id hqa)

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