α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
⊢ ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ b'), c i
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), i ∈ b → IsOpen (c i)
hc₂ : s ⊆ ⋃ (i : ι) (_ : i ∈ b), c i
⊢ ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ b'), c i
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
case intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ (i : ↑b) (_ : i ∈ d), c ↑i
⊢ ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ b'), c i
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
⊢ ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ b'), c i
rcases hs.elim_finite_subcover (fun i => c i : b → Set α) hc₁ hc₂ with ⟨d, hd⟩
case intro.refine'_1
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ (i : ↑b) (_ : i ∈ d), c ↑i
⊢ Subtype.val '' ↑d ⊆ b

case intro.refine'_2
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ (i : ↑b) (_ : i ∈ d), c ↑i
⊢ s ⊆ ⋃ (i : ι) (_ : i ∈ Subtype.val '' ↑d), c i
case intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ (i : ↑b) (_ : i ∈ d), c ↑i
⊢ ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ (i : ι) (_ : i ∈ b'), c i
refine' ⟨Subtype.val '' d.toSet, _, d.finite_toSet.image _, _⟩
no goals
case intro.refine'_1
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ (i : ↑b) (_ : i ∈ d), c ↑i
⊢ Subtype.val '' ↑d ⊆ b
simp
no goals
case intro.refine'_2
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.23729
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
b : Set ι
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ (x : ↑b), c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ (i : ↑b) (_ : i ∈ d), c ↑i
⊢ s ⊆ ⋃ (i : ι) (_ : i ∈ Subtype.val '' ↑d), c i
rwa [biUnion_image]