Commit 2025-09-16 21:53 241ba23e

View on Github →

chore(Topology): process porting notes (#29383) Go through the porting notes in the Topology folder and solve the ones with an obvious fix. This last batch of porting notes should bring us below 500 open porting notes in Mathlib, when the RingTheory ones get merged too!

Estimated changes

Modified Mathlib/Topology/Algebra/Module/CharacterSpace.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Algebra/MulAction.lean

Modified Mathlib/Topology/Algebra/Ring/Ideal.lean

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Bornology/Basic.lean

deleted def Bornology.cobounded

deleted theorem Bornology.le_cofinite

Modified Mathlib/Topology/Bornology/Constructions.lean

Modified Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Constructions/SumProd.lean

Modified Mathlib/Topology/ContinuousMap/Periodic.lean

Modified Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Homotopy/Basic.lean

Modified Mathlib/Topology/Homotopy/Equiv.lean

deleted def ContinuousMap.HomotopyEquiv.toFun'

deleted theorem ContinuousMap.HomotopyEquiv.toFun_eq_coe

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/LocallyConstant/Basic.lean

Modified Mathlib/Topology/MetricSpace/Algebra.lean

deleted def LipschitzAdd.C

Modified Mathlib/Topology/MetricSpace/Equicontinuity.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorff.lean

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

deleted theorem isometry_smul

Modified Mathlib/Topology/Order.lean

Modified Mathlib/Topology/Order/Compact.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/Sheaves/CommRingCat.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext

added theorem TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext

Modified Mathlib/Topology/Sheaves/Sheafify.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

deleted theorem UniformSpace.secondCountable_of_separable

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean