English
Let f be a smooth partition of unity on a set M, indexed by ι, subordinate to a family of sets U = {U_i}. Then for every i in ι we have the topological closure of the support of f_i contained in U_i; i.e., cl(supp f_i) ⊆ U_i.
Русский
Пусть f -- гладкое разбиение единств на множестве M, индексируемом ι, подчинённое семейству множеств U = {U_i}. Тогда для каждого i из ι выполняется: замыкание опоры f_i содержится в U_i; то есть cl(supp f_i) ⊆ U_i.
LaTeX
$$$\forall i, \operatorname{tsupport}(f_i) \subseteq U_i$$$
Lean4
/-- A smooth partition of unity `f i` is subordinate to a family of sets `U i` indexed by the same
type if for each `i` the closure of the support of `f i` is a subset of `U i`. -/
def IsSubordinate (f : SmoothPartitionOfUnity ι I M s) (U : ι → Set M) :=
∀ i, tsupport (f i) ⊆ U i
