IsSubordinate — Mathlib

English

For the constructed SmoothPartitionOfUnity from a BumpCovering, the i-th component equals the original partition's i-th component.

Русский

Для полученного из BumpCovering SmoothPartitionOfUnity i-я компонента равна i-й компоненте исходного разбиения.

LaTeX

$$$(f.toSmoothPartitionOfUnity hf i).toFun = f.toPartitionOfUnity i$.$$

Lean4

/-- We say that `f : SmoothBumpCovering ι I M s` is *subordinate* to a map `U : M → Set M` if for each
index `i`, we have `tsupport (f i) ⊆ U (f i).c`. This notion is a bit more general than
being subordinate to an open covering of `M`, because we make no assumption about the way `U x`
depends on `x`.
-/
def IsSubordinate {s : Set M} (f : SmoothBumpCovering ι I M s) (U : M → Set M) :=
  ∀ i, tsupport (f i) ⊆ U (f.c i)

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