Theorems · Theorem · general topology

LipschitzOnWith.extend_pi

∀ {α : Type u} {ι : Type x} [inst : PseudoMetricSpace α] [inst_1 : Fintype ι] {f : α → ι → ℝ} {s : Set α} {K : NNReal},
  LipschitzOnWith K f s → ∃ g, LipschitzWith K g ∧ Set.EqOn f g s

A function f : α → (ι → ℝ) which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space. The same result for the space ℓ^∞ (ι, ℝ) over a possibly infinite type ι is implemented in LipschitzOnWith.extend_lp_infty.

Defined in

Mathlib.Topology.MetricSpace.Lipschitz

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceFintype