cfcₙHom_continuous — Mathlib

English

Applying cfcₙHom to the identity function on the quasispectrum yields the original element a: cfcₙHom ha (.id (σₙ R a)) = a.

Русский

Применение cfcₙHom к тождественной функции на квазип спектре даёт исходный элемент a.

LaTeX

$$cfcₙHom ha (.id (σₙ R a)) = a$$

Lean4

@[fun_prop]
theorem cfcₙHom_continuous : Continuous (cfcₙHom ha : C(σₙ R a, R)₀ →⋆ₙₐ[R] A) :=
  cfcₙHom_isClosedEmbedding ha |>.continuous

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