α : Type u
β : Type v
X : Type ?u.546057
ι : Type ?u.546060
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : IsCompact s
⊢ ∃ t, t ∈ atTop ∧ (fun y => dist y x) ⁻¹' t ⊆ sᶜ
α : Type u
β : Type v
X : Type ?u.546057
ι : Type ?u.546060
inst✝ : PseudoMetricSpace α
x : α
⊢ comap (fun y => dist y x) atTop ≤ cocompact α
refine' Filter.hasBasis_cocompact.ge_iff.2 fun s hs => mem_comap.2 _
case intro
α : Type u
β : Type v
X : Type ?u.546057
ι : Type ?u.546060
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : IsCompact s
r : ℝ
hr : s ⊆ closedBall x r
⊢ ∃ t, t ∈ atTop ∧ (fun y => dist y x) ⁻¹' t ⊆ sᶜ
α : Type u
β : Type v
X : Type ?u.546057
ι : Type ?u.546060
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : IsCompact s
⊢ ∃ t, t ∈ atTop ∧ (fun y => dist y x) ⁻¹' t ⊆ sᶜ
rcases hs.bounded.subset_ball x with ⟨r, hr⟩
no goals
case intro
α : Type u
β : Type v
X : Type ?u.546057
ι : Type ?u.546060
inst✝ : PseudoMetricSpace α
x : α
s : Set α
hs : IsCompact s
r : ℝ
hr : s ⊆ closedBall x r
⊢ ∃ t, t ∈ atTop ∧ (fun y => dist y x) ⁻¹' t ⊆ sᶜ
exact ⟨Ioi r, Ioi_mem_atTop r, fun y hy hys => (mem_closedBall.1 <| hr hys).not_lt hy⟩