instContinuousMapUniqueHom — Mathlib

English

The quasispectrum-restriction mechanism preserves equality of restricted CFC maps under given embeddings and spectral hypotheses.

Русский

Механизм ограничения квази-спектра сохраняет равенство ограниченных карт CFC при заданных вложениях и спектральных предположениях.

LaTeX

$$$Eq (cfc g a) (cfc (\\lambda x. algebraMap(R,S)(g(f(x)))) a)$$$

Lean4

instance (priority := 100) instContinuousMapUniqueHom [TopologicalSpace A] [T2Space A] [Ring A] [StarRing A]
    [Algebra 𝕜 A] : ContinuousMap.UniqueHom 𝕜 A where
  eq_of_continuous_of_map_id s _ φ ψ hφ hψ
    h :=
    ContinuousMap.starAlgHom_ext_map_X hφ hψ <| by
      convert h using 1
      all_goals exact congr_arg _ (by ext; simp)

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