eventually_smallSets — Mathlib

English

For each x, eventually in the smallSets basis around x, the family {f_i ∩ s} is finite.

Русский

Для каждой точки x существует такая редукция вокруг x, что множество индексов с непустым пересечением конечное.

LaTeX

$$LocallyFinite f → ∀ x, ∀ᶠ s in (𝓝 x).smallSets, {i | (f i ∩ s).Nonempty}.Finite$$

Lean4

protected theorem eventually_smallSets (hf : LocallyFinite f) (x : X) :
    ∀ᶠ s in (𝓝 x).smallSets, {i | (f i ∩ s).Nonempty}.Finite :=
  locallyFinite_iff_smallSets.mp hf x

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