no goals
α : Type u
β : Type v
X : Type ?u.43642
ι : Type ?u.43645
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
x : α
⊢ (⋃ (n : ℕ), s ∩ closedBall x ↑n) = s
rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]