exists_finset_toPartitionOfUnity_eventuallyEq

English

There exists a finite set t such that near x, f.toPartitionOfUnity i equals f i times the finite product over t (with WellOrderingRel j i) of (1 − f j).

Русский

Существует конечное множество t, при котором около x выполняется равенство f^{PartitionOfUnity}_i = f_i ∙ ∏_{j∈t}(1 − f_j) для j, упорядованных относительно i.

LaTeX

$$$\exists t:\ Finset\, ι,\ f.toPartitionOfUnity_i =_{\mathcal{N}(x)} f_i \cdot \prod_{j \in t \text{ with } WellOrderingRel(j,i)} (1 - f_j)$$$

Lean4

theorem exists_finset_toPartitionOfUnity_eventuallyEq (i : ι) (x : X) :
    ∃ t : Finset ι, f.toPartitionOfUnity i =ᶠ[𝓝 x] f i * ∏ j ∈ t with WellOrderingRel j i, (1 - f j) :=
  f.exists_finset_toPOUFun_eventuallyEq i x

Похожие утверждения