Commit 2024-08-10 22:22 19796eea

View on Github →

feat(ContinuousMapZero): add norm structure on C(X, R)₀ (#15664) This PR adds a norm structure on C(X, R)₀. This is needed to work with integral representations of functions defined via the non-unital continuous functional calculus.

Estimated changes

Modified Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

added def ContinuousMapZero.evalCLM

added theorem ContinuousMapZero.evalCLM_apply

added def ContinuousMapZero.toContinuousMapCLM