Commit 2025-07-15 08:52 f68e1d93

View on Github →

chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra (#23498) Noticed while playing with the new directoryDependency linter. Not sure if these could be proved without assuming the continuity of real multiplication. Copyright from https://github.com/leanprover-community/mathlib3/pull/1921 and https://github.com/leanprover-community/mathlib4/pull/11840.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Group/AddTorsor.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Exp.lean

Created Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean

added theorem LipschitzOnWith.cauchySeq_comp

added theorem LipschitzWith.cauchySeq_comp

added theorem continuousAt_of_locally_lipschitz

Modified Mathlib/Topology/MetricSpace/Algebra.lean

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

deleted theorem LipschitzOnWith.cauchySeq_comp

deleted theorem LipschitzWith.cauchySeq_comp

deleted theorem continuousAt_of_locally_lipschitz

Modified Mathlib/Topology/MetricSpace/PiNat.lean