\import Algebra.Monoid
\import Algebra.Ordered
\import Arith.Real
\import Arith.Real.Field
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Topology.CoverSpace
\import Topology.MetricSpace
\open OrderedField

\record LipschitzMap (C : Real) (C>0 :  < C) \extends UniformMetricMap {
  | func-lipschitz {x y : Dom} : dist (func x) (func y) <= C * dist x y
  | func-dist-uniform {eps} eps>0 => inP (pinv C>0 * eps, OrderedSemiring.<_*_positive_positive (pinv>0 C>0) eps>0,
      \lam d => func-lipschitz <∘r transport (_ <) (inv *-assoc *> pmap (`* _) (pinv-right C>0) *> ide-left) (RealField.<_*_positive-right C>0 d))
  | func-cont {U} => defaultImpl PrecoverMap func-cont {_} {U}
}