Commit 2023-09-08 08:48 257d54b5

View on Github →

feat: a few lemmas on continuous functions (#7005) Topological prerequisites for Rademacher theorem in #7003.

Estimated changes

Modified Mathlib/Analysis/Complex/LocallyUniformLimit.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem HasCompactMulSupport.exists_bound_of_continuous

Modified Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

added theorem Continuous.clm_apply

added theorem ContinuousOn.clm_apply

Modified Mathlib/Topology/ContinuousOn.lean

added theorem ContinuousWithinAt.preimage_mem_nhdsWithin''

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean