toPartitionOfUnity — Mathlib

English

If a bump covering f is subordinate to a family U, then the resulting partition of unity is subordinate to U as well.

Русский

Если покрытие f является подпоркой к семейству U, тогда соответствующее разложение по единице подпорядковывается U.

LaTeX

$$f.IsSubordinate U → f.toPartitionOfUnity.IsSubordinate U$$

Lean4

theorem toPartitionOfUnity {f : BumpCovering ι X s} {U : ι → Set X} (h : f.IsSubordinate U) :
    f.toPartitionOfUnity.IsSubordinate U := fun i =>
  Subset.trans (closure_mono <| f.support_toPartitionOfUnity_subset i) (h i)

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