Commit 2023-02-24 13:10 481b74fd

View on Github →

feat: port Topology.UniformSpace.Compact (#2472)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/Compact.lean

added theorem CompactSpace.uniformContinuous_of_continuous

added theorem CompactSpace.uniformEquicontinuous_of_equicontinuous

added theorem Continuous.tendstoUniformly

added theorem Continuous.uniformContinuous_of_tendsto_cocompact

added theorem ContinuousOn.tendstoUniformly

added theorem HasCompactMulSupport.is_one_at_infty

added theorem HasCompactMulSupport.uniformContinuous_of_continuous

added theorem IsCompact.uniformContinuousAt_of_continuousAt

added theorem IsCompact.uniformContinuousOn_of_continuous

added theorem compactSpace_uniformity

added theorem nhdsSet_diagonal_eq_uniformity

added def uniformSpaceOfCompactT2

added theorem unique_uniformity_of_compact