α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
⊢ Set.Countable univ
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
⊢ Set.Countable univ
have := fun n => hf.finite_nonempty_inter_compact (isCompact_compactCovering α n)
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
i : ι
x✝ : i ∈ univ
⊢ i ∈ ⋃ (i : ℕ), {i_1 | Set.Nonempty (f i_1 ∩ compactCovering α i)}
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
⊢ Set.Countable univ
refine (countable_iUnion fun n => (this n).countable).mono fun i _ => ?_
case intro
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
i : ι
x✝ : i ∈ univ
x : α
hx : x ∈ f i
⊢ i ∈ ⋃ (i : ℕ), {i_1 | Set.Nonempty (f i_1 ∩ compactCovering α i)}
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
i : ι
x✝ : i ∈ univ
⊢ i ∈ ⋃ (i : ℕ), {i_1 | Set.Nonempty (f i_1 ∩ compactCovering α i)}
rcases hne i with ⟨x, hx⟩
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
i : ι
x✝ : i ∈ univ
x : α
hx : x ∈ f i
n : ℕ
hn : x ∈ compactCovering α n
⊢ i ∈ ⋃ (i : ℕ), {i_1 | Set.Nonempty (f i_1 ∩ compactCovering α i)}
case intro
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
i : ι
x✝ : i ∈ univ
x : α
hx : x ∈ f i
⊢ i ∈ ⋃ (i : ℕ), {i_1 | Set.Nonempty (f i_1 ∩ compactCovering α i)}
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩
no goals
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.163435
π : ι✝ → Type ?u.163440
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : SigmaCompactSpace α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
hne : ∀ (i : ι), Set.Nonempty (f i)
this : ∀ (n : ℕ), Set.Finite {i | Set.Nonempty (f i ∩ compactCovering α n)}
i : ι
x✝ : i ∈ univ
x : α
hx : x ∈ f i
n : ℕ
hn : x ∈ compactCovering α n
⊢ i ∈ ⋃ (i : ℕ), {i_1 | Set.Nonempty (f i_1 ∩ compactCovering α i)}
exact mem_iUnion.2 ⟨n, x, hx, hn⟩