toPartitionOfUnity — Mathlib

English

A smooth partition of unity can be regarded as a continuous partition of unity by taking the same component functions.

Русский

Гладкое разбиение единиц можно рассматривать как непрерывное разбиение единиц, взяв те же функции-компоненты.

LaTeX

$$$\mathrm{toPartitionOfUnity}(f) = \{ i \mapsto f_i \}_{i \in \iota}$, i.e. toPartitionOfUnity(f)(i) = f_i$$$

Lean4

/-- Reinterpret a smooth partition of unity as a continuous partition of unity. -/
@[simps]
def toPartitionOfUnity : PartitionOfUnity ι M s :=
  { f with toFun := fun i => f i }

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