cfcₙHom_eq_cfcₙHom_of_cfcHom — Mathlib

English

Under the unique-hom condition, cfc_nHom ha equals cfc_nHom_of_cfcHom R ha.

Русский

При условии уникальности гомоморфа, cfc_nHom ha равно cfc_nHom_of_cfcHom R ha.

LaTeX

$$$$ cfc\\!_nHom ha = cfc\\!_nHom\\_of\\_cfcHom R ha $$$$

Lean4

theorem cfcₙHom_eq_cfcₙHom_of_cfcHom [ContinuousMapZero.UniqueHom R A] {a : A} (ha : p a) :
    cfcₙHom (R := R) ha = cfcₙHom_of_cfcHom R ha :=
  by
  refine ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id (σₙ R a) _ _ ?_ ?_ ?_
  · exact (cfcₙHom_isClosedEmbedding (R := R) ha).continuous
  · exact (isClosedEmbedding_cfcₙHom_of_cfcHom ha).continuous
  · simpa only [cfcₙHom_id (R := R) ha] using (cfcHom_id ha).symm

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