toSmoothPartitionOfUnity_eq_mul_prod

English

There exists a finite subset t of the index set such that the i-th partition element equals φ_i(x) times the product over j in t of (1 − φ_j(x)) in a neighborhood of x.

Русский

Существует конечное множество t индексов, такое что при окрестности x элемент разбиения равен ⍴_i(x)·∏_{j∈t}(1−⍴_j(x)).

LaTeX

$$$\\exists t \\subseteq \\iota,\\; t \\text{ finite},\\; fs.toSmoothPartitionOfUnity\\, i\, x = fs i x \\cdot \\prod_{j \\in t \\text{ with } WellOrderingRel(j,i)} (1 - fs j x).$$$

Lean4

theorem toSmoothPartitionOfUnity_eq_mul_prod (i : ι) (x : M) (t : Finset ι)
    (ht : ∀ j, WellOrderingRel j i → fs j x ≠ 0 → j ∈ t) :
    fs.toSmoothPartitionOfUnity i x = fs i x * ∏ j ∈ t with WellOrderingRel j i, (1 - fs j x) :=
  fs.toBumpCovering.toPartitionOfUnity_eq_mul_prod i x t ht

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