English
For any p and a with pa, the image cfcₙAux hp₁ a ha f lies in the range of the inclusion inrNonUnitalStarAlgHom.
Русский
Образ cfcₙAux hp₁ a ha f принадлежит диапазону включения inrNonUnitalStarAlgHom.
LaTeX
$$$$ cfc\\_nAux hp\\_1 a ha f \\in \\operatorname{range}(\\text{inrNonUnitalStarAlgHom}) $$$$
Lean4
theorem cfcₙAux_mem_range_inr (f : C(σₙ 𝕜 a, 𝕜)₀) :
cfcₙAux hp₁ a ha f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A) :=
by
have h₁ :=
(isClosedEmbedding_cfcₙAux hp₁ a ha).continuous.range_subset_closure_image_dense
(ContinuousMapZero.adjoin_id_dense (σₙ 𝕜 a)) ⟨f, rfl⟩
rw [← SetLike.mem_coe]
refine closure_minimal ?_ ?_ h₁
· rw [← NonUnitalStarSubalgebra.coe_map, SetLike.coe_subset_coe, NonUnitalStarSubalgebra.map_le]
apply NonUnitalStarAlgebra.adjoin_le
apply Set.singleton_subset_iff.mpr
rw [SetLike.mem_coe, NonUnitalStarSubalgebra.mem_comap, cfcₙAux_id hp₁ a ha]
exact ⟨a, rfl⟩
· have : Continuous (Unitization.fst (R := 𝕜) (A := A)) := Unitization.uniformEquivProd.continuous.fst
simp only [NonUnitalStarAlgHom.coe_range]
convert IsClosed.preimage this (isClosed_singleton (x := 0))
aesop
