case inl
α : Type u
β : Type v
X : Type ?u.526468
ι : Type ?u.526471
inst✝¹ : PseudoMetricSpace α
x : α
t : Set α
r : ℝ
inst✝ : ProperSpace α
hc : IsClosed ∅
hb : Bounded ∅
⊢ IsCompact ∅

case inr.intro
α : Type u
β : Type v
X : Type ?u.526468
ι : Type ?u.526471
inst✝¹ : PseudoMetricSpace α
x✝ : α
s t : Set α
r : ℝ
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bounded s
x : α
⊢ IsCompact s
α : Type u
β : Type v
X : Type ?u.526468
ι : Type ?u.526471
inst✝¹ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bounded s
⊢ IsCompact s
rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
no goals
case inl
α : Type u
β : Type v
X : Type ?u.526468
ι : Type ?u.526471
inst✝¹ : PseudoMetricSpace α
x : α
t : Set α
r : ℝ
inst✝ : ProperSpace α
hc : IsClosed ∅
hb : Bounded ∅
⊢ IsCompact ∅
exact isCompact_empty
case inr.intro.intro
α : Type u
β : Type v
X : Type ?u.526468
ι : Type ?u.526471
inst✝¹ : PseudoMetricSpace α
x✝ : α
s t : Set α
r✝ : ℝ
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s
case inr.intro
α : Type u
β : Type v
X : Type ?u.526468
ι : Type ?u.526471
inst✝¹ : PseudoMetricSpace α
x✝ : α
s t : Set α
r : ℝ
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bounded s
x : α
⊢ IsCompact s
rcases hb.subset_ball x with ⟨r, hr⟩
no goals
case inr.intro.intro
α : Type u
β : Type v
X : Type ?u.526468
ι : Type ?u.526471
inst✝¹ : PseudoMetricSpace α
x✝ : α
s t : Set α
r✝ : ℝ
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s
exact isCompact_of_isClosed_subset (isCompact_closedBall x r) hc hr