α : Type u
β : Type v
X : Type ?u.280595
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
α : Type u
β : Type v
X : Type ?u.280595
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsCompact s
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t
refine' subset_countable_closure_of_almost_dense_set s fun ε hε => _
case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.280595
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : Set.Finite t
hst : s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
α : Type u
β : Type v
X : Type ?u.280595
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
X : Type ?u.280595
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : Set.Finite t
hst : s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => ball_subset_closedBall⟩