case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ r', (s ⊆ ⋃ (i : ι), ball (c i) (r' i)) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ r', (s ⊆ ⋃ (i : ι), ball (c i) (r' i)) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with
  ⟨v, hsv, hvc, hcv⟩
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r', r' ∈ Ioo 0 (r i) ∧ v i ⊆ ball (c i) r'
⊢ ∃ r', (s ⊆ ⋃ (i : ι), ball (c i) (r' i)) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ r', (s ⊆ ⋃ (i : ι), ball (c i) (r' i)) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
have := fun i => exists_pos_lt_subset_ball (hr i) (hvc i) (hcv i)
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', (s ⊆ ⋃ (i : ι), ball (c i) (r' i)) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r', r' ∈ Ioo 0 (r i) ∧ v i ⊆ ball (c i) r'
⊢ ∃ r', (s ⊆ ⋃ (i : ι), ball (c i) (r' i)) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
choose r' hlt hsub using this
no goals
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', (s ⊆ ⋃ (i : ι), ball (c i) (r' i)) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
exact ⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩