α : Type u
β : Type v
X : Type ?u.467547
ι : Type ?u.467550
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
s : Set α
⊢ Bounded s ↔ sᶜ ∈ (cobounded α).sets
α : Type u
β : Type v
X : Type ?u.467547
ι : Type ?u.467550
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
s : Set α
⊢ Bounded s ↔ IsBounded s
change Bounded s ↔ sᶜ ∈ (cobounded α).sets
no goals
α : Type u
β : Type v
X : Type ?u.467547
ι : Type ?u.467550
inst✝ : PseudoMetricSpace α
x : α
s✝ t : Set α
r : ℝ
s : Set α
⊢ Bounded s ↔ sᶜ ∈ (cobounded α).sets
simp [PseudoMetricSpace.cobounded_sets, Metric.Bounded]