eventually_fintsupport_subset

Mathlib.Geometry.Manifold.PartitionOfUnity

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

English

The finsupport is contained in finsupport under a Finset subset relation.

Русский

finsupport x0 подмножество finsupport x0 по отношению к Finset.

LaTeX

$$Finite.Subset relation on finsupport$$

Lean4

theorem eventually_fintsupport_subset : ∀ᶠ y in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀ :=
  ρ.toPartitionOfUnity.eventually_fintsupport_subset _

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

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

Разделы

Аффилиация

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