coe_toSmoothPartitionOfUnity — Mathlib

English

There is a canonical simplification Coe mapping between BumpCovering and SmoothPartitionOfUnity that preserves the i-th component.

Русский

Существует каноническое отображение между BumpCovering и SmoothPartitionOfUnity, сохраняющее i-ую компоненту.

LaTeX

$$$(f.toSmoothPartitionOfUnity hf)\_i = f_i$.$$

Lean4

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

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