α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.183504
α : Type u
inst✝ : UniformSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃ (i : ↑c), ↑i
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ∀ (y : α), (x, y) ∈ n → y ∈ t
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.183504
α : Type u
inst✝ : UniformSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ∀ (y : α), (x, y) ∈ n → y ∈ t
rw [sUnion_eq_iUnion] at hc₂
no goals
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.183504
α : Type u
inst✝ : UniformSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t
hc₂ : s ⊆ ⋃ (i : ↑c), ↑i
⊢ ∃ n, n ∈ 𝓤 α ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ ∀ (y : α), (x, y) ∈ n → y ∈ t
simpa using lebesgue_number_lemma hs (by simpa) hc₂
no goals
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.183504
α : Type u
inst✝ : UniformSpace α
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