finiteSupport — Mathlib

English

If X is a T2 space and U is compact, then the support of a locally finite function within U is finite.

Русский

Если X т2-пространство, а U компактно, опора локально конечной функции внутри U конечна.

LaTeX

$$$\\operatorname{finite}(\\operatorname{support}(D))$ under compactness of U and T2-space of X.$$

Lean4

/-- If `X` is T2 and if `U` is compact, then the support of a function with locally finite support
within `U` is finite.
-/
theorem finiteSupport [T2Space X] [Zero Y] (D : locallyFinsuppWithin U Y) (hU : IsCompact U) : Set.Finite D.support :=
  (hU.of_isClosed_subset (D.closedSupport hU.isClosed) D.supportWithinDomain).finite D.discreteSupport

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