Def ContinuousMapZero.evalCLM

Modification history

2024-12-11 08:26

Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

feat(Topology/ContinuousMap): "ContinuousMap.evalCLM" without compactness (#19876) …

Modified ContinuousMapZero.evalCLM View on Github →

2024-08-10 22:22

Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

feat(ContinuousMapZero): add norm structure on `C(X, R)₀` (#15664) …

Added ContinuousMapZero.evalCLM View on Github →