no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
s : Set α
⊢ LipschitzOnWith K f s ↔ LipschitzWith K (restrict s f)
simp only [LipschitzOnWith, LipschitzWith, SetCoe.forall', restrict, Subtype.edist_eq]