Theorems · Definition · general topology

LipschitzOnWith

{α : Type u} → {β : Type v} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → NNReal → (α → β) → Set α → Prop

A function f is Lipschitz continuous with constant K ≥ 0 on `s` if for all x, y in s we have dist (f x) (f y) ≤ K * dist x y.

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

164 results in Mathlib

Foundations

Depth 147 from the axioms, rests on 3,160 definitions · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpace