locallyFinite — Mathlib

English

The supports of the partition pieces form a locally finite family: for every x in X, only finitely many i have x in the support of f_i.

Русский

Опорные множества частей разбиения образуют локально конечное семейство: для каждого x в X существует конечное множество индексов i, таких что x принадлежит опоре f_i.

LaTeX

$$$\text{LocallyFinite }(i \mapsto \operatorname{support}(f_i))$; equivalently, for every $x \in X$, the set $\{i \mid x \in \operatorname{supp}(f_i)\}$ is finite.$$

Lean4

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

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