Theorems · Definition · general topology

LipschitzWith

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

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

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

316 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace