Def LocallyLipschitz

Modification history

2024-07-18 00:30

Mathlib/Topology/EMetricSpace/Lipschitz.lean

feat: Locally Lipschitz functions on a set (#13990) …

Modified LocallyLipschitz View on Github →

2023-11-08 08:49

Mathlib/Topology/EMetricSpace/Lipschitz.lean

chore(Lipschitz): split (#8264) …

Modified LocallyLipschitz View on Github →

2023-09-26 14:05

Mathlib/Topology/MetricSpace/Lipschitz.lean

feat: locally Lipschitz maps (#7314) …

Added LocallyLipschitz View on Github →