α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
⊢ Set.Finite {i | Set.Nonempty (f i ∩ s)}
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
ι : Type u_1
f : ι → Set α
hf : LocallyFinite f
s : Set α
hs : IsCompact s
⊢ Set.Finite {i | Set.Nonempty (f i ∩ s)}
choose U hxU hUf using hf
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ Set.Finite {i | Set.Nonempty (f i ∩ s)}
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
⊢ Set.Finite {i | Set.Nonempty (f i ∩ s)}
rcases hs.elim_nhds_subcover U fun x _ => hxU x with ⟨t, -, hsU⟩
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ {i | Set.Nonempty (f i ∩ s)} ⊆ ⋃ (i : α) (_ : i ∈ ↑t), {i_1 | Set.Nonempty (f i_1 ∩ U i)}
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ Set.Finite {i | Set.Nonempty (f i ∩ s)}
refine' (t.finite_toSet.biUnion fun x _ => hUf x).subset _
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
i : ι
x : α
hx : x ∈ f i ∩ s
⊢ i ∈ ⋃ (i : α) (_ : i ∈ ↑t), {i_1 | Set.Nonempty (f i_1 ∩ U i)}
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ {i | Set.Nonempty (f i ∩ s)} ⊆ ⋃ (i : α) (_ : i ∈ ↑t), {i_1 | Set.Nonempty (f i_1 ∩ U i)}
rintro i ⟨x, hx⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
i : ι
x : α
hx : x ∈ f i ∩ s
c : α
hct : c ∈ t
hcx : x ∈ U c
⊢ i ∈ ⋃ (i : α) (_ : i ∈ ↑t), {i_1 | Set.Nonempty (f i_1 ∩ U i)}
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
i : ι
x : α
hx : x ∈ f i ∩ s
⊢ i ∈ ⋃ (i : α) (_ : i ∈ ↑t), {i_1 | Set.Nonempty (f i_1 ∩ U i)}
rcases mem_iUnion₂.1 (hsU hx.2) with ⟨c, hct, hcx⟩
no goals
case intro.intro.intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.20320
π : ι✝ → Type ?u.20325
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ : Set α
ι : Type u_1
f : ι → Set α
s : Set α
hs : IsCompact s
U : α → Set α
hxU : ∀ (x : α), U x ∈ 𝓝 x
hUf : ∀ (x : α), Set.Finite {i | Set.Nonempty (f i ∩ U x)}
t : Finset α
hsU : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
i : ι
x : α
hx : x ∈ f i ∩ s
c : α
hct : c ∈ t
hcx : x ∈ U c
⊢ i ∈ ⋃ (i : α) (_ : i ∈ ↑t), {i_1 | Set.Nonempty (f i_1 ∩ U i)}
exact mem_biUnion hct ⟨x, hx.1, hcx⟩