support_subset — Mathlib

English

If f is a SmoothBumpCovering subordinate to U, then the support of each f_i is contained in a local neighborhood determined by U, and the family {supp f_i} is locally finite.

Русский

Если f — SmoothBumpCovering, подчинённое U, то опора каждой f_i лежит в локальном окружении, сумма опор локально конечна.

LaTeX

$$$\forall i, \operatorname{supp}(f_i) \subseteq U_i$ and $\{\operatorname{supp}(f_i)\}_{i}$ is locally finite.$$

Lean4

theorem support_subset {fs : SmoothBumpCovering ι I M s} {U : M → Set M} (h : fs.IsSubordinate U) (i : ι) :
    support (fs i) ⊆ U (fs.c i) :=
  Subset.trans subset_closure (h i)

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