case intro.intro
α : Type u
β : Type v
ι : Type ?u.75608
π : ι → Type ?u.75613
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t✝ : Set α
inst✝ : CompactSpace α
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x
t : Finset α
s : univ ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ ∃ t, (⋃ (x : α) (_ : x ∈ t), U x) = ⊤
α : Type u
β : Type v
ι : Type ?u.75608
π : ι → Type ?u.75613
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x
⊢ ∃ t, (⋃ (x : α) (_ : x ∈ t), U x) = ⊤
obtain ⟨t, -, s⟩ := IsCompact.elim_nhds_subcover isCompact_univ U fun x _ => hU x
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.75608
π : ι → Type ?u.75613
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t✝ : Set α
inst✝ : CompactSpace α
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x
t : Finset α
s : univ ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ ∃ t, (⋃ (x : α) (_ : x ∈ t), U x) = ⊤
exact ⟨t, top_unique s⟩