English
A family of sets f: ι → Set X is locally finite if for every x ∈ X there exists a neighborhood t of x such that only finitely many f(i) meet t.
Русский
Семейство множеств f: ι → Set X локально конечно, если для каждого x ∈ X существует окрестность t(x) такая, что лишь конечное число i удовлетворяет f(i) ∩ t ≠ ∅.
LaTeX
$$$\\forall x\\in X, \\exists t\\in \\mathcal{N}(x), \\#\\{ i \\mid (f(i) \\cap t) \\neq \\emptyset \\} < \\infty$$$
Lean4
/-- A family of sets in `Set X` is locally finite if at every point `x : X`,
there is a neighborhood of `x` which meets only finitely many sets in the family. -/
def LocallyFinite (f : ι → Set X) :=
∀ x : X, ∃ t ∈ 𝓝 x, {i | (f i ∩ t).Nonempty}.Finite
