Commit 2024-08-29 08:05 11329efd

View on Github →

feat: the space of continuous maps is complete if the target is complete (#16224)

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean

Modified Mathlib/Topology/ContinuousFunction/Compact.lean

Modified Mathlib/Topology/RestrictGenTopology.lean

added theorem RestrictGenTopology.isCompact_of_weaklyLocallyCompact

added theorem RestrictGenTopology.of_nhds

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

added theorem ContinuousMap.completeSpace_of_restrictGenTopology

added theorem ContinuousMap.range_toUniformOnFunIsCompact