Theorem UniformOnFun.lipschitzWith_one_ofFun_toFun

Modification history

2025-06-19 08:56
Mathlib/Topology/MetricSpace/UniformConvergence.lean
feat: define a metric structure on `α →ᵤ β` (#25827) …
Added UniformOnFun.lipschitzWith_one_ofFun_toFunView on Github →