point_finite

Mathlib.Topology.PartitionOfUnity

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

English

For any x ∈ X, the set {i | f_i(x) ≠ 0} is finite.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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