[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f✝ f g : PartitionOfUnity ι X s
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f g : PartitionOfUnity ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ (x : X), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), ↑(toFun✝ i) x ≤ 1
h : (mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝).toFun = g.toFun
⊢ mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i => support ↑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
sum_eq_one'✝¹ : ∀ (x : X), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝¹ i) x = 1
sum_le_one'✝¹ : ∀ (x : X), ∑ᶠ (i : ι), ↑(toFun✝¹ i) x ≤ 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ (x : X), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), ↑(toFun✝ i) x ≤ 1
h :
  (mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ sum_eq_one'✝¹ sum_le_one'✝¹).toFun =
    (mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝).toFun
⊢ mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ sum_eq_one'✝¹ sum_le_one'✝¹ =
    mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ ∃ i, 0 < ↑(↑f i) x
[PROOFSTEP]
have H := f.sum_eq_one hx
[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∑ᶠ (i : ι), ↑(↑f i) x = 1
⊢ ∃ i, 0 < ↑(↑f i) x
[PROOFSTEP]
contrapose! H
[GOAL]
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (i : ι), ↑(↑f i) x ≤ 0
⊢ ∑ᶠ (i : ι), ↑(↑f i) x ≠ 1
[PROOFSTEP]
simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f✝ f g : BumpCovering ι X s
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f g : BumpCovering ι X s
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ (x : X), x ∈ s → ∃ i, ↑(toFun✝ i) =ᶠ[𝓝 x] 1
h : (mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝).toFun = g.toFun
⊢ mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i => support ↑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
le_one'✝¹ : toFun✝¹ ≤ 1
eventuallyEq_one'✝¹ : ∀ (x : X), x ∈ s → ∃ i, ↑(toFun✝¹ i) =ᶠ[𝓝 x] 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ (x : X), x ∈ s → ∃ i, ↑(toFun✝ i) =ᶠ[𝓝 x] 1
h :
  (mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ le_one'✝¹ eventuallyEq_one'✝¹).toFun =
    (mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝).toFun
⊢ mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ le_one'✝¹ eventuallyEq_one'✝¹ =
    mk s toFun✝ locallyFinite'✝ nonneg'✝ le_one'✝ eventuallyEq_one'✝
[PROOFSTEP]
congr
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i_1 | Set.Nonempty ((fun i_2 => support ↑(Pi.single i 1 i_2)) i_1 ∩ t)}
[PROOFSTEP]
refine' ⟨univ, univ_mem, (finite_singleton i).subset _⟩
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
⊢ {i_1 | Set.Nonempty ((fun i_2 => support ↑(Pi.single i 1 i_2)) i_1 ∩ univ)} ⊆ {i}
[PROOFSTEP]
rintro j ⟨x, hx, -⟩
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x✝ : X
j : ι
x : X
hx : x ∈ (fun i_1 => support ↑(Pi.single i 1 i_1)) j
⊢ j ∈ {i}
[PROOFSTEP]
contrapose! hx
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x✝ : X
j : ι
x : X
hx : ¬j ∈ {i}
⊢ ¬x ∈ support ↑(Pi.single i 1 j)
[PROOFSTEP]
rw [mem_singleton_iff] at hx 
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x✝ : X
j : ι
x : X
hx : ¬j = i
⊢ ¬x ∈ support ↑(Pi.single i 1 j)
[PROOFSTEP]
simp [hx]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
x✝ : x ∈ s
⊢ ↑(Pi.single i 1 i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
rw [Pi.single_eq_same, ContinuousMap.coe_one]
[GOAL]
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases exists_subset_iUnion_closure_subset hs ho (fun x _ => hf.point_finite x) hU with ⟨V, hsV, hVo, hVU⟩
[GOAL]
case intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
have hVU' : ∀ i, V i ⊆ U i := fun i => Subset.trans subset_closure (hVU i)
[GOAL]
case intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases exists_subset_iUnion_closure_subset hs hVo (fun x _ => (hf.subset hVU').point_finite x) hsV with
  ⟨W, hsW, hWo, hWV⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
choose f hfp hf0 hf1 hf01 using fun i =>
  h01 _ _ (isClosed_compl_iff.2 <| hVo i) isClosed_closure (disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
have hsupp : ∀ i, support (f i) ⊆ V i := fun i => support_subset_iff'.2 (hf0 i)
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ↑(f i) ⊆ V i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
refine'
  ⟨⟨f, hf.subset fun i => Subset.trans (hsupp i) (hVU' i), fun i x => (hf01 i x).1, fun i x => (hf01 i x).2, fun x hx =>
      _⟩,
    hfp, fun i => Subset.trans (closure_mono (hsupp i)) (hVU i)⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ↑(f i) ⊆ V i
x : X
hx : x ∈ s
⊢ ∃ i, ↑(f i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
s : Set X
f✝ : BumpCovering ι X s
inst✝ : NormalSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ (i : ι), U i
V : ι → Set X
hsV : s ⊆ iUnion V
hVo : ∀ (i : ι), IsOpen (V i)
hVU : ∀ (i : ι), closure (V i) ⊆ U i
hVU' : ∀ (i : ι), V i ⊆ U i
W : ι → Set X
hsW : s ⊆ iUnion W
hWo : ∀ (i : ι), IsOpen (W i)
hWV : ∀ (i : ι), closure (W i) ⊆ V i
f : ι → C(X, ℝ)
hfp : ∀ (i : ι), p ↑(f i)
hf0 : ∀ (i : ι), EqOn (↑(f i)) 0 (V i)ᶜ
hf1 : ∀ (i : ι), EqOn (↑(f i)) 1 (closure (W i))
hf01 : ∀ (i : ι) (x : X), ↑(f i) x ∈ Icc 0 1
hsupp : ∀ (i : ι), support ↑(f i) ⊆ V i
x : X
hx : x ∈ s
i : ι
hi : x ∈ W i
⊢ ∃ i, ↑(f i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
exact ⟨i, ((hf1 i).mono subset_closure).eventuallyEq_of_mem ((hWo i).mem_nhds hi)⟩
[GOAL]
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
[GOAL]
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
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
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, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
rcases exists_isSubordinate_of_locallyFinite_of_prop p h01 hs V hVo hVf hsV with ⟨f, hfp, hf⟩
[GOAL]
case intro.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
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
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
hfp : ∀ (i : ι), p ↑(↑f i)
hf : IsSubordinate f V
⊢ ∃ f, (∀ (i : ι), p ↑(↑f i)) ∧ IsSubordinate f U
[PROOFSTEP]
exact ⟨f, hfp, hf.mono hVU⟩
[GOAL]
ι : 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
[PROOFSTEP]
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩
[GOAL]
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
[PROOFSTEP]
rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨f, hf.mono hVU⟩
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
h : ↑(↑f i) x = 0
⊢ toPOUFun f i x = 0
[PROOFSTEP]
rw [toPOUFun, h, zero_mul]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
⊢ toPOUFun f i x = ↑(↑f i) x * ∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(↑f j) x)
[PROOFSTEP]
refine' congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => _)
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
j : ι
hj : 1 - ↑(↑f j) x ≠ 1
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
[PROOFSTEP]
rw [Ne.def, sub_eq_self] at hj 
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(↑f j) x = 0
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
[PROOFSTEP]
rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
t : Finset ι
ht : ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(↑f j) x = 0
⊢ WellOrderingRel j i → j ∈ t
[PROOFSTEP]
exact flip (ht j) hj
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
set s := (f.point_finite x).toFinset
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
have hs : (s : Set ι) = {i | f i x ≠ 0} := Finite.coe_toFinset _
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
have A : (support fun i => toPOUFun f i x) ⊆ s := by
  rw [hs]
  exact fun i hi => f.support_toPOUFun_subset i hi
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
⊢ (support fun i => toPOUFun f i x) ⊆ ↑s
[PROOFSTEP]
rw [hs]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
⊢ (support fun i => toPOUFun f i x) ⊆ {i | ↑(↑f i) x ≠ 0}
[PROOFSTEP]
exact fun i hi => f.support_toPOUFun_subset i hi
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
have B : (mulSupport fun i => 1 - f i x) ⊆ s :=
  by
  rw [hs, mulSupport_one_sub]
  exact fun i => id
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
⊢ (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
[PROOFSTEP]
rw [hs, mulSupport_one_sub]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
⊢ (support fun i => ↑(↑f i) x) ⊆ {i | ↑(↑f i) x ≠ 0}
[PROOFSTEP]
exact fun i => id
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
letI : LinearOrder ι := linearOrderOfSTO WellOrderingRel
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ᶠ (i : ι), toPOUFun f i x = 1 - ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B, Finset.prod_one_sub_ordered,
  sub_sub_cancel]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ i in s, toPOUFun f i x = ∑ i in s, ↑(↑f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(↑f j) x)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i _ => _
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝ : i ∈ s
⊢ toPOUFun f i x = ↑(↑f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(↑f j) x)
[PROOFSTEP]
convert f.toPOUFun_eq_mul_prod _ _ _ fun j _ hj => _
[GOAL]
case convert_4
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(↑f i) x ≠ 0})
hs : ↑s = {i | ↑(↑f i) x ≠ 0}
A : (support fun i => toPOUFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(↑f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝¹ : i ∈ s
j : ι
x✝ : WellOrderingRel j i
hj : ↑(↑f j) x ≠ 0
⊢ j ∈ s
[PROOFSTEP]
rwa [Finite.mem_toFinset]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
⊢ ∃ t, toPOUFun f i =ᶠ[𝓝 x] ↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑f j))
[PROOFSTEP]
rcases f.locallyFinite x with ⟨U, hU, hf⟩
[GOAL]
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
⊢ ∃ t, toPOUFun f i =ᶠ[𝓝 x] ↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑f j))
[PROOFSTEP]
use hf.toFinset
[GOAL]
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
⊢ toPOUFun f i =ᶠ[𝓝 x] ↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - ↑f j))
[PROOFSTEP]
filter_upwards [hU] with y hyU
[GOAL]
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPOUFun f i y = (↑(↑f i) * ↑(∏ j in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), (1 - ↑f j))) y
[PROOFSTEP]
simp only [ContinuousMap.coe_prod, Pi.mul_apply, Finset.prod_apply]
[GOAL]
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ toPOUFun f i y = ↑(↑f i) y * ∏ c in Finset.filter (fun j => WellOrderingRel j i) (Finite.toFinset hf), ↑(1 - ↑f c) y
[PROOFSTEP]
apply toPOUFun_eq_mul_prod
[GOAL]
case h.ht
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
⊢ ∀ (j : ι), WellOrderingRel j i → ↑(↑f j) y ≠ 0 → j ∈ Finite.toFinset hf
[PROOFSTEP]
intro j _ hj
[GOAL]
case h.ht
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : Set.Finite {i | Set.Nonempty ((fun i => support ↑(↑f i)) i ∩ U)}
y : X
hyU : y ∈ U
j : ι
a✝ : WellOrderingRel j i
hj : ↑(↑f j) y ≠ 0
⊢ j ∈ Finite.toFinset hf
[PROOFSTEP]
exact hf.mem_toFinset.2 ⟨y, ⟨hj, hyU⟩⟩
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ Continuous (toPOUFun f i)
[PROOFSTEP]
refine' (f i).continuous.mul <| continuous_finprod_cond (fun j _ => continuous_const.sub (f j).continuous) _
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => mulSupport fun x => 1 - ↑(↑f i) x
[PROOFSTEP]
simp only [mulSupport_one_sub]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
⊢ LocallyFinite fun i => support fun x => ↑(↑f i) x
[PROOFSTEP]
exact f.locallyFinite
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ ∑ᶠ (i : ι), ↑((fun i => ContinuousMap.mk (toPOUFun f i)) i) x = 1
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_eq_self]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ ∏ᶠ (i : ι), (1 - ↑(↑f i) x) = 0
[PROOFSTEP]
apply finprod_eq_zero (fun i => 1 - f i x) (f.ind x hx)
[GOAL]
case hx
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ 1 - ↑(↑f (ind f x hx)) x = 0
[PROOFSTEP]
simp only [f.ind_apply x hx, sub_self]
[GOAL]
case hf
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ Set.Finite (mulSupport fun i => 1 - ↑(↑f i) x)
[PROOFSTEP]
rw [mulSupport_one_sub]
[GOAL]
case hf
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ Set.Finite (support fun i => ↑(↑f i) x)
[PROOFSTEP]
exact f.point_finite x
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ ∑ᶠ (i : ι), ↑((fun i => ContinuousMap.mk (toPOUFun f i)) i) x ≤ 1
[PROOFSTEP]
simp only [ContinuousMap.coe_mk, sum_toPOUFun_eq, sub_le_self_iff]
[GOAL]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
⊢ 0 ≤ ∏ᶠ (i : ι), (1 - ↑(↑f i) x)
[PROOFSTEP]
exact finprod_nonneg fun i => sub_nonneg.2 <| f.le_one i x
