finsupport_subset_fintsupport

Mathlib.Geometry.Manifold.PartitionOfUnity

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

English

Sum over a Finset equals finsum over all indices.

Русский

Сумма по конечному множеству равно бесконечной сумме по всем индексам.

LaTeX

$$$(\sum i \in I, f_i(x)) = \sum^\infty_i f_i(x)$$$

Lean4

theorem finsupport_subset_fintsupport : ρ.finsupport x₀ ⊆ ρ.fintsupport x₀ :=
  ρ.toPartitionOfUnity.finsupport_subset_fintsupport x₀

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

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

Разделы

Аффилиация

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