ext_continuousMap — Mathlib

English

The spectral image of cfcₙHom ha f coincides with the range of f on the spectrum.

Русский

Спектральное отображение cfcₙHom ha f совпадает с образованием f на спектре.

LaTeX

$$σₙ R (cfcₙHom ha f) = Set.range (ContinuousMapZero.instFunLike.coe f)$$

Lean4

theorem ext_continuousMap [UniqueHom R A] (a : A) [CompactSpace (σₙ R a)] (φ ψ : C(σₙ R a, R)₀ →⋆ₙₐ[R] A)
    (hφ : Continuous φ) (hψ : Continuous ψ) (h : φ (.id (σₙ R a)) = ψ (.id (σₙ R a))) : φ = ψ :=
  UniqueHom.eq_of_continuous_of_map_id _ φ ψ hφ hψ h

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