Commit 2024-05-29 16:56 377e7e02

View on Github →

feat: the non-unital star subalgebra generated by id is dense in C(s, 𝕜)₀ (#13326) This is a version of the Weierstrass approximation theorem for C(s, 𝕜)₀, and is necessary for instances of the non-unital continuous functional calculus. Co-authored by: @adedecker

depends on: #13323

Estimated changes

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

added def ContinuousMap.evalAlgHom

added def ContinuousMap.evalStarAlgHom

Modified Mathlib/Topology/ContinuousFunction/Polynomial.lean

added theorem Polynomial.toContinuousMapOn_X_eq_restrict_id

added theorem Polynomial.toContinuousMap_X_eq_id

Modified Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean

added theorem ContinuousMap.AlgHom.closure_ker_inter

added theorem ContinuousMap.adjoin_id_eq_span_one_add

added theorem ContinuousMap.adjoin_id_eq_span_one_union

added theorem ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id

added theorem ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id

added theorem ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom

added theorem ContinuousMapZero.adjoin_id_dense