ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
ι : 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 - ↑(toFun s f i) x
set s := (f.point_finite x).toFinset
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
have hs : (s : Set ι) = { i | f i x ≠ 0 } := Finite.coe_toFinset _
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
have A : (support fun i => toPouFun f i x) ⊆ s := by
  rw [hs]
  exact fun i hi => f.support_toPouFun_subset i hi
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
have B : (mulSupport fun i => 1 - f i x) ⊆ s := by
  rw [hs, mulSupport_one_sub]
  exact fun i => id
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
letI : LinearOrder ι := linearOrderOfSTO WellOrderingRel
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ i in s, toPouFun f i x =
    ∑ i in s, ↑(toFun s✝ f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(toFun s✝ f j) x)
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ (∑ᶠ (i : ι), toPouFun f i x) = 1 - ∏ᶠ (i : ι), 1 - ↑(toFun s✝ f i) x
rw [finsum_eq_sum_of_support_subset _ A, finprod_eq_prod_of_mulSupport_subset _ B,
  Finset.prod_one_sub_ordered, sub_sub_cancel]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝ : i ∈ s
⊢ toPouFun f i x = ↑(toFun s✝ f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(toFun s✝ f j) x)
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ i in s, toPouFun f i x =
    ∑ i in s, ↑(toFun s✝ f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(toFun s✝ f j) x)
refine' Finset.sum_congr rfl fun i _ => _
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 | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝¹ : i ∈ s
j : ι
x✝ : WellOrderingRel j i
hj : ↑(toFun s✝ f j) x ≠ 0
⊢ j ∈ s
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝ : i ∈ s
⊢ toPouFun f i x = ↑(toFun s✝ f i) x * ∏ j in Finset.filter (fun x => x < i) s, (1 - ↑(toFun s✝ f j) x)
convert f.toPouFun_eq_mul_prod _ _ _ fun j _ hj => _
no goals
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 | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
B : (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
i : ι
x✝¹ : i ∈ s
j : ι
x✝ : WellOrderingRel j i
hj : ↑(toFun s✝ f j) x ≠ 0
⊢ j ∈ s
rwa [Finite.mem_toFinset]
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
⊢ (support fun i => toPouFun f i x) ⊆ {i | ↑(toFun s✝ f i) x ≠ 0}
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
⊢ (support fun i => toPouFun f i x) ⊆ ↑s
rw [hs]
no goals
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
⊢ (support fun i => toPouFun f i x) ⊆ {i | ↑(toFun s✝ f i) x ≠ 0}
exact fun i hi => f.support_toPouFun_subset i hi
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
⊢ (support fun i => ↑(toFun s✝ f i) x) ⊆ {i | ↑(toFun s✝ f i) x ≠ 0}
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
⊢ (mulSupport fun i => 1 - ↑(toFun s✝ f i) x) ⊆ ↑s
rw [hs, mulSupport_one_sub]
no goals
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := Finite.toFinset (_ : Set.Finite {i | ↑(toFun s✝ f i) x ≠ 0})
hs : ↑s = {i | ↑(toFun s✝ f i) x ≠ 0}
A : (support fun i => toPouFun f i x) ⊆ ↑s
⊢ (support fun i => ↑(toFun s✝ f i) x) ⊆ {i | ↑(toFun s✝ f i) x ≠ 0}
exact fun i => id