Locally finite families of sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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.at_top 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.