point_finite

Mathlib.Geometry.Manifold.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#SmoothBumpCovering.point_finite

English

For each x, the set {i | fs i x ≠ 0} is finite.

Русский

Для каждого x множество {i | fs_i(x) ≠ 0} конечно.

LaTeX

$$$\{i \mid fs_i(x) \neq 0\}.\Finite$$$

Lean4

protected theorem point_finite (x : M) : {i | fs i x ≠ 0}.Finite :=
  fs.locallyFinite.point_finite x

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

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

Разделы

Аффилиация

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