case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, IsSubordinate f U
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ f, IsSubordinate f U
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
case intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : IsSubordinate f V
⊢ ∃ f, IsSubordinate f U
case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, IsSubordinate f U
rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩
no goals
case intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ (i : ι), V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : IsSubordinate f V
⊢ ∃ f, IsSubordinate f U
exact ⟨f, hf.mono hVU⟩