Commit 2024-11-19 16:30 53523844

View on Github →

chore: split Topology.UniformSpace.Basic (#19194) and reorganize material in UniformSpace.Compact (moving some material from Basic into it, and splitting parts of the original content out into later files)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/UniformGroup/Basic.lean

Modified Mathlib/Topology/Algebra/UniformGroup/Defs.lean

Modified Mathlib/Topology/EMetricSpace/Defs.lean

Modified Mathlib/Topology/GDelta/UniformSpace.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

deleted theorem Disjoint.exists_uniform_thickening

deleted theorem Disjoint.exists_uniform_thickening_of_basis

deleted theorem IsCompact.nhdsSet_basis_uniformity

deleted theorem lebesgue_number_lemma

deleted theorem lebesgue_number_lemma_sUnion

deleted theorem lebesgue_number_of_compact_open

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

Modified Mathlib/Topology/UniformSpace/Compact.lean

deleted theorem CompactSpace.uniformContinuous_of_continuous

deleted theorem CompactSpace.uniformEquicontinuous_of_equicontinuous

deleted theorem Continuous.tendstoUniformly

deleted theorem Continuous.uniformContinuous_of_tendsto_cocompact

deleted theorem ContinuousOn.tendstoUniformly

added theorem Disjoint.exists_uniform_thickening

added theorem Disjoint.exists_uniform_thickening_of_basis

deleted theorem HasCompactMulSupport.uniformContinuous_of_continuous

deleted theorem IsCompact.mem_uniformity_of_prod

added theorem IsCompact.nhdsSet_basis_uniformity

deleted theorem IsCompact.uniformContinuousAt_of_continuousAt

deleted theorem IsCompact.uniformContinuousOn_of_continuous

added theorem lebesgue_number_lemma

added theorem lebesgue_number_lemma_sUnion

added theorem lebesgue_number_of_compact_open

deleted def uniformSpaceOfCompactT2

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

Created Mathlib/Topology/UniformSpace/HeineCantor.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.uniformContinuous_of_continuous

added theorem IsCompact.mem_uniformity_of_prod

added theorem IsCompact.uniformContinuousAt_of_continuousAt

added theorem IsCompact.uniformContinuousOn_of_continuous

Created Mathlib/Topology/UniformSpace/OfCompactT2.lean

added def uniformSpaceOfCompactT2

Modified Mathlib/Topology/UniformSpace/OfFun.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean