English
Induction principle for star-valued continuous maps on compact s; extension from previous induction principle.
Русский
Индуктивный принцип для звездных непрерывных отображений на компактном s; продолжение предыдущей индукции.
LaTeX
$$$\text{InductionOnOfCompact}(s)$.$$
Lean4
/-- If `s : Set 𝕜` with `RCLike 𝕜` is compact and contains `0`, then the non-unital star subalgebra
generated by the identity function in `C(s, 𝕜)₀` is dense. This can be seen as a version of the
Weierstrass approximation theorem. -/
theorem adjoin_id_dense (s : Set 𝕜) [Fact (0 ∈ s)] [CompactSpace s] :
Dense (adjoin 𝕜 {(.id s : C(s, 𝕜)₀)} : Set C(s, 𝕜)₀) :=
by
have h0' : 0 ∈ s := Fact.out
rw [dense_iff_closure_eq, ← isClosedEmbedding_toContinuousMap.injective.preimage_image (closure _), ←
isClosedEmbedding_toContinuousMap.closure_image_eq, ← coe_toContinuousMapHom, ← NonUnitalStarSubalgebra.coe_map,
NonUnitalStarAlgHom.map_adjoin_singleton, toContinuousMapHom_apply, toContinuousMap_id, ←
ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id s h0']
apply Set.eq_univ_of_forall fun f ↦ ?_
simp only [Set.mem_preimage, toContinuousMapHom_apply, SetLike.mem_coe, RingHom.mem_ker,
ContinuousMap.evalStarAlgHom_apply, ContinuousMap.coe_coe]
exact map_zero f
