English
The composition of the inr embedding with cfc_Hom equals cfc_Hom auxiliary map.
Русский
Композиция вложения вr и cfc_Hom равна вспомогательной карте.
LaTeX
$$(inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux (isStarNormal_inr (R := ℂ) (A := A)) a ha$$
Lean4
theorem inr_comp_cfcₙHom_eq_cfcₙAux {A : Type*} [NonUnitalCStarAlgebra A] (a : A) [ha : IsStarNormal a] :
(inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux (isStarNormal_inr (R := ℂ) (A := A)) a ha :=
by
have h (a : A) := isStarNormal_inr (R := ℂ) (A := A) (a := a)
refine
@ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id _ _ _ _ _ _ _ _ _ _ _ inferInstance inferInstance _ (σₙ ℂ a)
_ _ _ _ ?_ ?_ ?_
· change Continuous (fun f ↦ (cfcₙHom ha f : A⁺¹)); fun_prop
· exact isClosedEmbedding_cfcₙAux (@(h)) a ha |>.continuous
· trans (a : A⁺¹)
· congrm (inr $(cfcₙHom_id ha))
· exact cfcₙAux_id (@(h)) a ha |>.symm
