α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
⊢ cocompact ((d : δ) → κ d) ≤ Filter.coprodᵢ fun d => cocompact (κ d)
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
⊢ (Filter.coprodᵢ fun d => cocompact (κ d)) = cocompact ((d : δ) → κ d)
refine' le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) _
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s✝ t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
s : Set ((i : δ) → κ i)
H : sᶜ ∈ Filter.coprodᵢ fun d => cocompact (κ d)
⊢ sᶜ ∈ cocompact ((d : δ) → κ d)
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
⊢ cocompact ((d : δ) → κ d) ≤ Filter.coprodᵢ fun d => cocompact (κ d)
refine' compl_surjective.forall.2 fun s H => _
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s✝ t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
s : Set ((i : δ) → κ i)
H : ∀ (i : δ), ∃ t, IsCompact t ∧ s ⊆ Function.eval i ⁻¹' t
⊢ ∃ t, IsCompact t ∧ s ⊆ t
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s✝ t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
s : Set ((i : δ) → κ i)
H : sᶜ ∈ Filter.coprodᵢ fun d => cocompact (κ d)
⊢ sᶜ ∈ cocompact ((d : δ) → κ d)
simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H⊢
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s✝ t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
s : Set ((i : δ) → κ i)
K : (i : δ) → Set (κ i)
hKc : ∀ (i : δ), IsCompact (K i)
htK : ∀ (i : δ), s ⊆ Function.eval i ⁻¹' K i
⊢ ∃ t, IsCompact t ∧ s ⊆ t
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s✝ t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
s : Set ((i : δ) → κ i)
H : ∀ (i : δ), ∃ t, IsCompact t ∧ s ⊆ Function.eval i ⁻¹' t
⊢ ∃ t, IsCompact t ∧ s ⊆ t
choose K hKc htK using H
no goals
α : Type u
β : Type v
ι : Type ?u.140164
π : ι → Type ?u.140169
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
s✝ t : Set α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
δ : Type u_1
κ : δ → Type u_2
inst✝ : (d : δ) → TopologicalSpace (κ d)
s : Set ((i : δ) → κ i)
K : (i : δ) → Set (κ i)
hKc : ∀ (i : δ), IsCompact (K i)
htK : ∀ (i : δ), s ⊆ Function.eval i ⁻¹' K i
⊢ ∃ t, IsCompact t ∧ s ⊆ t
exact ⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩