sum_finsupport

Mathlib.Geometry.Manifold.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#SmoothPartitionOfUnity.sum_finsupport

English

The finsupport of ρ at x0 is contained in itself under inclusion.

Русский

finsupport(ρ, x0) ⊆ finsupport(ρ, x0).

LaTeX

$$$\rho.finsupport x_0 \subseteq \rho.finsupport x_0$$$

Lean4

theorem sum_finsupport (hx₀ : x₀ ∈ s) : ∑ i ∈ ρ.finsupport x₀, ρ i x₀ = 1 :=
  ρ.toPartitionOfUnity.sum_finsupport hx₀

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru