no goals
α : Type u
β : Type v
X : Type ?u.46280
ι : Type ?u.46283
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s✝ s : Set α
⊢ IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
  compl_compl]