supportLocallyFiniteWithinDomain — Mathlib

English

For each z in U, there exists a neighborhood U_z such that U_z intersects the support of the function in a finite set.

Русский

Для каждого z в U существует окрестность U_z такая, что U_z пересечение опоры функции конечна.

LaTeX

$$$\\forall z \\in U,\\ \\exists t \\in \\mathcal{N}(z),\\ \\#(t \\cap \\operatorname{support}(D))<\\infty$$$

Lean4

theorem supportLocallyFiniteWithinDomain [Zero Y] (D : locallyFinsuppWithin U Y) :
    ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ D.support) :=
  D.supportLocallyFiniteWithinDomain'

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