Theorems · Theorem · general topology

LipschitzWith.lipschitzOnWith

∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
  {s : Set α}, LipschitzWith K f → LipschitzOnWith K f s

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

16 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace