support_toPOUFun_subset — Mathlib

English

For each index i, the support of the i-th bump function used in the partition of unity is contained in the support of the original bump function f_i.

Русский

Для каждого индекса i опора i-й функции-импульса разбиения по единице вложена в опору исходной функции f_i.

LaTeX

$$$\operatorname{supp}(f^{\mathrm{POU}}_i) \subseteq \operatorname{supp}(f_i)$$$

Lean4

theorem support_toPOUFun_subset (i : ι) : support (f.toPOUFun i) ⊆ support (f i) := fun _ =>
  mt <| f.toPOUFun_zero_of_zero

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