α : Type u
β : Type v
X : Type ?u.453997
ι : Type ?u.454000
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃ (i : ↑c), ↑i
⊢ ∃ δ, δ > 0 ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ball x δ ⊆ t
α : Type u
β : Type v
X : Type ?u.453997
ι : Type ?u.454000
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ δ, δ > 0 ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ball x δ ⊆ t
rw [sUnion_eq_iUnion] at hc₂
no goals
α : Type u
β : Type v
X : Type ?u.453997
ι : Type ?u.454000
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃ (i : ↑c), ↑i
⊢ ∃ δ, δ > 0 ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ball x δ ⊆ t
simpa using lebesgue_number_lemma_of_metric hs (by simpa) hc₂
no goals
α : Type u
β : Type v
X : Type ?u.453997
ι : Type ?u.454000
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃ (i : ↑c), ↑i
⊢ ∀ (i : ↑c), IsOpen ↑i
simpa