Theorems · Definition · general topology

LocallyLipschitz

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

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

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

34 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace