fintsupport

Mathlib.Geometry.Manifold.PartitionOfUnity

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

← MathLib Explorer

English

The finsupport at x0 is a subset of the finsupport set at x0.

Русский

finsupport x0 ⊆ finsupport x0 как множество индексов.

LaTeX

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

Lean4

/-- The tsupport of a partition of unity at a point `x₀` as a `Finset`.
This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/
def fintsupport (x : M) : Finset ι :=
  (ρ.finite_tsupport x).toFinset

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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