support_toSmoothPartitionOfUnity_subset

English

The support of the smooth partition element φ_i is contained in the support of the i-th bump function.

Русский

Опора функции разбиения φ_i содержится внутри опоры i-й шип-функции.

LaTeX

$$$\\operatorname{supp}(fs.toSmoothPartitionOfUnity(i)) \\subseteq \\operatorname{supp}(fs(i)).$$$

Lean4

theorem support_toSmoothPartitionOfUnity_subset (i : ι) : support (fs.toSmoothPartitionOfUnity i) ⊆ support (fs i) :=
  fs.toBumpCovering.support_toPartitionOfUnity_subset i

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