Def ContinuousMapZero.toContinuousMapCLM

Modification history

2024-08-10 22:22
Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean
feat(ContinuousMapZero): add norm structure on `C(X, R)₀` (#15664) …
Added ContinuousMapZero.toContinuousMapCLMView on Github →