ι : 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 → ↑(toFun s f j) x ≠ 0 → j ∈ t
j : ι
hj : 1 - ↑(toFun s f j) x ≠ 1
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
ι : 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 → ↑(toFun s f j) x ≠ 0 → j ∈ t
⊢ toPouFun f i x = ↑(toFun s f i) x * ∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(toFun s f j) x)
refine' congr_arg _ (finprod_cond_eq_prod_of_cond_iff _ fun {j} hj => _)
ι : 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 → ↑(toFun s f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(toFun s f j) x = 0
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
ι : 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 → ↑(toFun s f j) x ≠ 0 → j ∈ t
j : ι
hj : 1 - ↑(toFun s f j) x ≠ 1
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
rw [Ne.def, sub_eq_self] at hj
ι : 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 → ↑(toFun s f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(toFun s f j) x = 0
⊢ WellOrderingRel j i → j ∈ t
ι : 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 → ↑(toFun s f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(toFun s f j) x = 0
⊢ WellOrderingRel j i ↔ j ∈ Finset.filter (fun j => WellOrderingRel j i) t
rw [Finset.mem_filter, Iff.comm, and_iff_right_iff_imp]
no goals
ι : 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 → ↑(toFun s f j) x ≠ 0 → j ∈ t
j : ι
hj : ¬↑(toFun s f j) x = 0
⊢ WellOrderingRel j i → j ∈ t
exact flip (ht j) hj