case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vc : (⋃ (i : Option ι), v i) = univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' (sᶜ) u a
⊢ ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ (s ⊆ ⋃ (i : ι), v i) ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
⊢ ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ (s ⊆ ⋃ (i : ι), v i) ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
rcases precise_refinement (Option.elim' (sᶜ) u) (Option.forall.2 ⟨isOpen_compl_iff.2 hs, uo⟩)
    uc with
  ⟨v, vo, vc, vf, vu⟩
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vc : (⋃ (i : Option ι), v i) = univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' (sᶜ) u a
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vc : (⋃ (i : Option ι), v i) = univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' (sᶜ) u a
⊢ ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ (s ⊆ ⋃ (i : ι), v i) ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
refine' ⟨v ∘ some, fun i ↦ vo _, _, vf.comp_injective (Option.some_injective _), fun i ↦ vu _⟩
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ univ ⊆ ⋃ (i : Option ι), Option.elim' (sᶜ) u i
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
apply Subset.antisymm (subset_univ _)
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ sᶜ ∪ s ⊆ sᶜ ∪ ⋃ (a : ι), u a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ univ ⊆ ⋃ (i : Option ι), Option.elim' (sᶜ) u i
simp_rw [← compl_union_self s, Option.elim', iUnion_option]
no goals
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ sᶜ ∪ s ⊆ sᶜ ∪ ⋃ (a : ι), u a
apply union_subset_union_right (sᶜ) us
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' (sᶜ) u a
vc : v noneᶜ ⊆ ⋃ (i : ι), v (some i)
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vc : (⋃ (i : Option ι), v i) = univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' (sᶜ) u a
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i
simp only [iUnion_option, ← compl_subset_iff_union] at vc
no goals
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : (⋃ (i : Option ι), Option.elim' (sᶜ) u i) = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' (sᶜ) u a
vc : v noneᶜ ⊆ ⋃ (i : ι), v (some i)
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i
exact Subset.trans (subset_compl_comm.1 <| vu Option.none) vc