ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => mulSupport fun x => 1 - ↑(toFun s f i) x
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ Continuous (toPouFun f i)
refine' (f i).continuous.mul <|
  continuous_finprod_cond (fun j _ => continuous_const.sub (f j).continuous) _
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => support fun x => ↑(toFun s f i) x
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => mulSupport fun x => 1 - ↑(toFun s f i) x
simp only [mulSupport_one_sub]
no goals
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => support fun x => ↑(toFun s f i) x
exact f.locallyFinite