instFunLikeContMDiffMapRealModelWithCornersSelfSomeENatTop

English

A smooth partition of unity indexed by ι is locally finite when the supports of its members are locally finite.

Русский

Разбиение единства с индексами ι гладкое и локально конечное, когда поддержи его членов локально конечны.

LaTeX

$$$LocallyFinite\\ (i \\mapsto \\operatorname{support}(f_i))$$$

Lean4

instance {s : Set M} : FunLike (SmoothPartitionOfUnity ι I M s) ι C^∞⟮I, M; 𝓘(ℝ), ℝ⟯
    where
  coe := toFun
  coe_injective' f g h := by cases f; cases g; congr

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