exists_finset_toSmoothPartitionOfUnity_eventuallyEq

English

For any i, x, and finite t, if t contains exactly the indices j with j ≺ i and φ_j(x) ≠ 0, then φ_i(x) = φ_i(x) · ∏_{j ∈ t, j ≺ i} (1 − φ_j(x)).

Русский

Для любого i, x и конечного множества t, если t содержит ровно те индексы j, для которых j ≺ i и φ_j(x) ≠ 0, то φ_i(x) = φ_i(x) · ∏_{j ∈ t, j ≺ i} (1 − φ_j(x)).

LaTeX

$$$fs.toSmoothPartitionOfUnity_i(x) = fs_i(x) \\cdot \\prod_{j \\in t \\text{ with } WellOrderingRel(j,i)} (1 - fs_j(x)).$$$

Lean4

theorem exists_finset_toSmoothPartitionOfUnity_eventuallyEq (i : ι) (x : M) :
    ∃ t : Finset ι,
      fs.toSmoothPartitionOfUnity i =ᶠ[𝓝 x] fs i * ∏ j ∈ t with WellOrderingRel j i, ((1 : M → ℝ) - fs j) :=
  by simpa using fs.toBumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq i x

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