Theorem UniformOnFun.lipschitzWith_restrict

Modification history

2025-07-04 07:44
Mathlib/Topology/MetricSpace/UniformConvergence.lean
chore: further whitespace fixes (#26708) …
Modified UniformOnFun.lipschitzWith_restrictView on Github →
2025-06-19 08:56
Mathlib/Topology/MetricSpace/UniformConvergence.lean
feat: define a metric structure on `α →ᵤ β` (#25827) …
Added UniformOnFun.lipschitzWith_restrictView on Github →