Commit 2024-06-18 12:22 05a03c38
View on Github →feat(Topology/ContinuousFunction/CompactlySupported) bundle the class of compactly supported continuous functions (#12402) give definitions of the class of compactly supported continuous functions and prove basic properties. Motivation: This class is most natural for the domain of the Riesz-Markov-Kakutani theorem #12290 I copied Mathlib.Topology.ContinuousFunction.ZeroAtInfty and am trying to adapt it to compactly supported functions.