Theorem LipschitzOnWith.cauchySeq_comp

Modification history

2025-07-15 08:52
Mathlib/Topology/Algebra/MetricSpace/Lipschitz.lean
chore(Topology.MetricSpace.Lipschitz): stop depending on Topology.Algebra (#23498) …
Modified LipschitzOnWith.cauchySeq_compView on Github →
2024-04-03 09:14
Mathlib/Topology/MetricSpace/Lipschitz.lean
feat: drop completeness assumptions in theorems involving integrals (#11840) …
Added LipschitzOnWith.cauchySeq_compView on Github →