locallyFinite — Mathlib

English

There exists a locally finite cover by supports of the partition of unity functions, ensuring good local behavior.

Русский

Существует локально конечное покрытие опор функций разбиения едности, обеспечивающее хорошее локальное поведение.

LaTeX

$$LocallyFinite( f_i )$$

Lean4

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

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