Commit 2024-10-20 13:19 6cd5a568
View on Github →feat: induction principles for ContinuousMap via Stone-Weierstrass (#17831)
This PR provides induction lemmas for C(s, 𝕜) and C(s, 𝕜)₀ with RCLike 𝕜. The idea is that when s is compact, the closure hypothesis will follow from the Stone-Weierstrass theorem and a limit property of the motive p.