coe_finsupport

Mathlib.Geometry.Manifold.PartitionOfUnity

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

English

For a fixed x0, the set {i | x0 ∈ tsupport (ρ i)} is finite.

Русский

Для фиксированной точки x0 множество индексов i с x0 ∈ tsupport (ρ i) конечное.

LaTeX

$$$\{ i \mid x_0 \in tsupport(\rho i) \}.\text{Finite}$$$

Lean4

@[simp]
theorem coe_finsupport : (ρ.finsupport x₀ : Set ι) = support fun i ↦ ρ i x₀ :=
  ρ.toPartitionOfUnity.coe_finsupport x₀

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

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

Разделы

Аффилиация

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