isClosedEmbedding_cfcₙAux — Mathlib

English

The map cfcₙAux hp₁ a ha is a closed embedding into the unitization, i.e., it is a topological embedding with closed image.

Русский

Отображение cfcₙAux hp₁ a ha является замкнутым вложением в единичное расширение: топологическое вложение с замкнутым образом образа.

LaTeX

$$$$ \\text{IsClosedEmbedding}\\bigl(cfc\\_nAux hp\\_1 a ha\\bigr) $$$$

Lean4

theorem isClosedEmbedding_cfcₙAux : IsClosedEmbedding (cfcₙAux hp₁ a ha) :=
  by
  simp only [cfcₙAux, NonUnitalStarAlgHom.coe_comp]
  refine ((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp ContinuousMapZero.isClosedEmbedding_toContinuousMap
  let e : C(σₙ 𝕜 a, 𝕜) ≃ₜ C(σ 𝕜 (a : A⁺¹), 𝕜) :=
    (Homeomorph.setCongr (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a)).arrowCongr (.refl _)
  exact e.isClosedEmbedding

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