α✝ : Type ?u.431840
β✝ : Type ?u.431843
γ : Type ?u.431846
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed (⋂ (i : α) (_ : i ∈ s) (i_1 : α) (_ : i_1 ∈ s), {x | edist (x i) (x i_1) ≤ ↑K * edist i i_1})
α✝ : Type ?u.431840
β✝ : Type ?u.431843
γ : Type ?u.431846
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed {f | LipschitzOnWith K f s}
simp only [LipschitzOnWith, setOf_forall]
case refine'_1
α✝ : Type ?u.431840
β✝ : Type ?u.431843
γ : Type ?u.431846
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => edist (x_1 x) (x_1 y)

case refine'_2
α✝ : Type ?u.431840
β✝ : Type ?u.431843
γ : Type ?u.431846
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => ↑K * edist x y
α✝ : Type ?u.431840
β✝ : Type ?u.431843
γ : Type ?u.431846
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed (⋂ (i : α) (_ : i ∈ s) (i_1 : α) (_ : i_1 ∈ s), {x | edist (x i) (x i_1) ≤ ↑K * edist i i_1})
refine' isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le _ _
no goals
case refine'_1
α✝ : Type ?u.431840
β✝ : Type ?u.431843
γ : Type ?u.431846
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => edist (x_1 x) (x_1 y)

case refine'_2
α✝ : Type ?u.431840
β✝ : Type ?u.431843
γ : Type ?u.431846
inst✝² : PseudoEMetricSpace α✝
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
x : α
x✝¹ : x ∈ s
y : α
x✝ : y ∈ s
⊢ Continuous fun x_1 => ↑K * edist x y
exacts [.edist (continuous_apply x) (continuous_apply y), continuous_const]