toSmoothPartitionOfUnity_toPartitionOfUnity

English

The underlying partition of unity of a SmoothPartitionOfUnity coincides with the original partition of unity.

Русский

Базовая разбиение единиц SmoothPartitionOfUnity совпадает с исходным разбиением единиц.

LaTeX

$$$(f^{\mathrm{PU}}) = f.toPartitionOfUnity$ as partitions of unity.$$

Lean4

@[simp]
theorem toSmoothPartitionOfUnity_toPartitionOfUnity (f : BumpCovering ι M s) (hf : ∀ i, ContMDiff I 𝓘(ℝ) ∞ (f i)) :
    (f.toSmoothPartitionOfUnity hf).toPartitionOfUnity = f.toPartitionOfUnity :=
  rfl

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