α : Type u
β : Type v
ι : Type ?u.155649
π : ι → Type ?u.155654
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ (⋃ (x : ℕ), Exists.choose (_ : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ (⋃ (n : ℕ), K n) = univ) x) = univ
α : Type u
β : Type v
ι : Type ?u.155649
π : ι → Type ?u.155654
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ (⋃ (n : ℕ), compactCovering α n) = univ
rw [compactCovering, iUnion_accumulate]
no goals
α : Type u
β : Type v
ι : Type ?u.155649
π : ι → Type ?u.155654
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ (⋃ (x : ℕ), Exists.choose (_ : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ (⋃ (n : ℕ), K n) = univ) x) = univ
exact (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2