English
There exists a finite set t of indices such that the i-th POU function equals the i-th bump function multiplied by the finite product over t, in a neighborhood of x.
Русский
Существует конечное множество индексов t, для которого вокруг точки x выполняется равенство: f^{POU}_i = f_i · ∏_{j∈t} (1 − f_j).
LaTeX
$$$\exists t:\ Finset\, ι,\ f^{\mathrm{POU}}_i =_{\mathcal{N}(x)} f_i \cdot \prod_{j \in t \text{ with } WellOrderingRel(j,i)} (1 - f_j)$$$
Lean4
theorem exists_finset_toPOUFun_eventuallyEq (i : ι) (x : X) :
∃ t : Finset ι, f.toPOUFun i =ᶠ[𝓝 x] f i * ∏ j ∈ t with WellOrderingRel j i, (1 - f j) :=
by
rcases f.locallyFinite x with ⟨U, hU, hf⟩
use hf.toFinset
filter_upwards [hU] with y hyU
simp only [ContinuousMap.coe_prod, Pi.mul_apply, Finset.prod_apply]
apply toPOUFun_eq_mul_prod
intro j _ hj
exact hf.mem_toFinset.2 ⟨y, ⟨hj, hyU⟩⟩
