# mathlibdocumentation

topology.locally_finite

### 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.

def locally_finite {ι : Type u_1} {X : Type u_4} (f : ι → set X) :
Prop

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
theorem locally_finite_of_finite {ι : Type u_1} {X : Type u_4} [finite ι] (f : ι → set X) :
theorem locally_finite.point_finite {ι : Type u_1} {X : Type u_4} {f : ι → set X} (hf : locally_finite f) (x : X) :
{b : ι | x f b}.finite
@[protected]
theorem locally_finite.subset {ι : Type u_1} {X : Type u_4} {f g : ι → set X} (hf : locally_finite f) (hg : ∀ (i : ι), g i f i) :
theorem locally_finite.comp_inj_on {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} {f : ι → set X} {g : ι' → ι} (hf : locally_finite f) (hg : {i : ι' | (f (g i)).nonempty}) :
theorem locally_finite.comp_injective {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} {f : ι → set X} {g : ι' → ι} (hf : locally_finite f) (hg : function.injective g) :
theorem locally_finite.eventually_finite {ι : Type u_1} {X : Type u_4} {f : ι → set X} (hf : locally_finite f) (x : X) :
∀ᶠ (s : set X) in (nhds x).small_sets, {i : ι | (f i s).nonempty}.finite
theorem locally_finite.exists_mem_basis {ι : Type u_1} {X : Type u_4} {f : ι → set X} {ι' : Sort u_2} (hf : locally_finite f) {p : ι' → Prop} {s : ι' → set X} {x : X} (hb : (nhds x).has_basis p s) :
∃ (i : ι') (hi : p i), {j : ι | (f j s i).nonempty}.finite
theorem locally_finite.sum_elim {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} {f : ι → set X} {g : ι' → set X} (hf : locally_finite f) (hg : locally_finite g) :
@[protected]
theorem locally_finite.closure {ι : Type u_1} {X : Type u_4} {f : ι → set X} (hf : locally_finite f) :
locally_finite (λ (i : ι), closure (f i))
theorem locally_finite.is_closed_Union {ι : Type u_1} {X : Type u_4} {f : ι → set X} (hf : locally_finite f) (hc : ∀ (i : ι), is_closed (f i)) :
is_closed (⋃ (i : ι), f i)
theorem locally_finite.closure_Union {ι : Type u_1} {X : Type u_4} {f : ι → set X} (h : locally_finite f) :
closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
theorem locally_finite.Inter_compl_mem_nhds {ι : Type u_1} {X : Type u_4} {f : ι → set X} (hf : locally_finite f) (hc : ∀ (i : ι), is_closed (f i)) (x : X) :
(⋂ (i : ι) (hi : x f i), (f i)) nhds x

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.

theorem locally_finite.exists_forall_eventually_eq_prod {X : Type u_4} {π : X → Sort u_1} {f : Π (x : X), π x} (hf : locally_finite (λ (n : ), {x : X | f (n + 1) x f n x})) :
∃ (F : Π (x : X), π x), ∀ (x : X), ∀ᶠ (p : × X) in , f p.fst p.snd = F p.snd

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.

theorem locally_finite.exists_forall_eventually_at_top_eventually_eq' {X : Type u_4} {π : X → Sort u_1} {f : Π (x : X), π x} (hf : locally_finite (λ (n : ), {x : X | f (n + 1) x f n x})) :
∃ (F : Π (x : X), π x), ∀ (x : X), ∀ᶠ (n : ) in filter.at_top, ∀ᶠ (y : X) in nhds x, f n y = F y

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.

theorem locally_finite.exists_forall_eventually_at_top_eventually_eq {α : Type u_3} {X : Type u_4} {f : X → α} (hf : locally_finite (λ (n : ), {x : X | f (n + 1) x f n x})) :
∃ (F : X → α), ∀ (x : X), ∀ᶠ (n : ) in filter.at_top, f n =ᶠ[nhds x] F

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.

theorem locally_finite.preimage_continuous {ι : Type u_1} {X : Type u_4} {Y : Type u_5} {f : ι → set X} {g : Y → X} (hf : locally_finite f) (hg : continuous g) :
locally_finite (λ (i : ι), g ⁻¹' f i)