Locally finite families of sets #
We say that a family of sets in a topological space is locally finite if at every point x : X,
there is a neighborhood of x which meets only finitely many sets in the family.
In this file we give the definition and prove basic properties of locally finite families of sets.
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.
Equations
- LocallyFinite f = ∀ (x : X), ∃ t, t ∈ nhds x ∧ Set.Finite { i | Set.Nonempty (f i ∩ t) }
If f : β → set α is a locally finite family of closed sets, then for any x : α, the
intersection of the complements to f i, x ∉ f i, is a neighbourhood of x.
Let f : ℕ → Π a, β a be a sequence of (dependent) functions on a topological space. Suppose
that the family of sets s n = {x | f (n + 1) x ≠ f n x} is locally finite. Then there exists a
function F : Π a, β a such that for any x, we have f n x = F x on the product of an infinite
interval [N, +∞) and a neighbourhood of x.
We formulate the conclusion in terms of the product of filter Filter.atTop and 𝓝 x.
Let f : ℕ → Π a, β a be a sequence of (dependent) functions on a topological space. Suppose
that the family of sets s n = {x | f (n + 1) x ≠ f n x} is locally finite. Then there exists a
function F : Π a, β a such that for any x, for sufficiently large values of n, we have
f n y = F y in a neighbourhood of x.
Let f : ℕ → α → β be a sequence of functions on a topological space. Suppose
that the family of sets s n = {x | f (n + 1) x ≠ f n x} is locally finite. Then there exists a
function F : α → β such that for any x, for sufficiently large values of n, we have
f n =ᶠ[𝓝 x] F.