Theorems · Definition · general topology

LocallyLipschitzOn

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

f : α → β is called locally Lipschitz continuous on s iff every point x of s has a neighbourhood within s on which f is Lipschitz.

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

29 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpace