locallyFinite

Mathlib.Topology.PartitionOfUnity

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

English

The family of supports i ↦ supp(f_i) is locally finite.

Русский

Семейство поддержек i ↦ supp(f_i) локально конечное.

LaTeX

$$$$\operatorname{LocallyFinite}\\left( i \mapsto \operatorname{supp}(f_i)\right).$$$$

Lean4

protected theorem locallyFinite : LocallyFinite fun i => support (f i) :=
  f.locallyFinite'

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

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

Разделы

Аффилиация

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