no goals
α✝ : Type ?u.433749
β✝ : Type ?u.433752
γ : Type ?u.433755
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
⊢ IsClosed {f | LipschitzWith K f}
simp only [← lipschitz_on_univ, isClosed_setOf_lipschitzOnWith]