Commit 2024-03-08 18:41 158514fb

View on Github →

feat(UniformSpace/CompactConvergence): prove metrizability (#10942)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/Order/Filter/Bases.lean

deleted theorem Filter.HasAntitoneBasis.map

added theorem Filter.HasBasis.isCountablyGenerated

modified theorem Filter.isCountablyGenerated_seq

Modified Mathlib/Topology/Algebra/UniformGroup.lean

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

added theorem CompactExhaustion.exists_superset_of_isCompact

Created Mathlib/Topology/Metrizable/ContinuousMap.lean

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

added theorem CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity

added theorem CompactExhaustion.hasBasis_compactConvergenceUniformity

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean