α : Type u
β : Type v
ι : Type ?u.165278
π : ι → Type ?u.165283
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝[univ] x
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
α : Type u
β : Type v
ι : Type ?u.165278
π : ι → Type ?u.165283
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
simp only [← nhdsWithin_univ] at hf
case intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.165278
π : ι → Type ?u.165283
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : SigmaCompactSpace α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝[univ] x
s : Set α
hsc : Set.Countable s
hsU : univ ⊆ ⋃ (x : α) (_ : x ∈ s), f x
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
α : Type u
β : Type v
ι : Type ?u.165278
π : ι → Type ?u.165283
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝[univ] x
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
rcases countable_cover_nhdsWithin_of_sigma_compact isClosed_univ fun x _ => hf x with
  ⟨s, -, hsc, hsU⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.165278
π : ι → Type ?u.165283
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
inst✝ : SigmaCompactSpace α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝[univ] x
s : Set α
hsc : Set.Countable s
hsU : univ ⊆ ⋃ (x : α) (_ : x ∈ s), f x
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
exact ⟨s, hsc, univ_subset_iff.1 hsU⟩