# Documentation

## Mathlib.Topology.LocallyFinite

### 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 LocallyFinite {ι : Type u_1} {X : Type u_4} [] (f : ιSet X) :

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
• = ∀ (x : X), tnhds x, {i : ι | (f i t).Nonempty}.Finite
Instances For
theorem locallyFinite_of_finite {ι : Type u_1} {X : Type u_4} [] [] (f : ιSet X) :
theorem LocallyFinite.point_finite {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) (x : X) :
{b : ι | x f b}.Finite
theorem LocallyFinite.subset {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} {g : ιSet X} (hf : ) (hg : ∀ (i : ι), g i f i) :
theorem LocallyFinite.comp_injOn {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [] {f : ιSet X} {g : ι'ι} (hf : ) (hg : Set.InjOn g {i : ι' | (f (g i)).Nonempty}) :
theorem LocallyFinite.comp_injective {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [] {f : ιSet X} {g : ι'ι} (hf : ) (hg : ) :
theorem locallyFinite_iff_smallSets {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} :
∀ (x : X), ∀ᶠ (s : Set X) in (nhds x).smallSets, {i : ι | (f i s).Nonempty}.Finite
theorem LocallyFinite.eventually_smallSets {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) (x : X) :
∀ᶠ (s : Set X) in (nhds x).smallSets, {i : ι | (f i s).Nonempty}.Finite
theorem LocallyFinite.exists_mem_basis {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} {ι' : Sort u_6} (hf : ) {p : ι'Prop} {s : ι'Set X} {x : X} (hb : (nhds x).HasBasis p s) :
∃ (i : ι'), p i {j : ι | (f j s i).Nonempty}.Finite
theorem LocallyFinite.nhdsWithin_iUnion {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) (a : X) :
nhdsWithin a (⋃ (i : ι), f i) = ⨆ (i : ι), nhdsWithin a (f i)
theorem LocallyFinite.continuousOn_iUnion' {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [] [] {f : ιSet X} {g : XY} (hf : ) (hc : ∀ (i : ι), xclosure (f i), ContinuousWithinAt g (f i) x) :
ContinuousOn g (⋃ (i : ι), f i)
theorem LocallyFinite.continuousOn_iUnion {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [] [] {f : ιSet X} {g : XY} (hf : ) (h_cl : ∀ (i : ι), IsClosed (f i)) (h_cont : ∀ (i : ι), ContinuousOn g (f i)) :
ContinuousOn g (⋃ (i : ι), f i)
theorem LocallyFinite.continuous' {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [] [] {f : ιSet X} {g : XY} (hf : ) (h_cov : ⋃ (i : ι), f i = Set.univ) (hc : ∀ (i : ι), xclosure (f i), ContinuousWithinAt g (f i) x) :
theorem LocallyFinite.continuous {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [] [] {f : ιSet X} {g : XY} (hf : ) (h_cov : ⋃ (i : ι), f i = Set.univ) (h_cl : ∀ (i : ι), IsClosed (f i)) (h_cont : ∀ (i : ι), ContinuousOn g (f i)) :
theorem LocallyFinite.closure {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) :
LocallyFinite fun (i : ι) => closure (f i)
theorem LocallyFinite.closure_iUnion {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (h : ) :
closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
theorem LocallyFinite.isClosed_iUnion {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) (hc : ∀ (i : ι), IsClosed (f i)) :
IsClosed (⋃ (i : ι), f i)
theorem LocallyFinite.iInter_compl_mem_nhds {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) (hc : ∀ (i : ι), IsClosed (f i)) (x : X) :
⋂ (i : ι), ⋂ (_ : xf 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 LocallyFinite.exists_forall_eventually_eq_prod {X : Type u_4} [] {π : XSort u_6} {f : (x : X) → π x} (hf : LocallyFinite fun (n : ) => {x : X | f (n + 1) x f n x}) :
∃ (F : (x : X) → π x), ∀ (x : X), ∀ᶠ (p : × X) in Filter.atTop ×ˢ nhds x, f p.1 p.2 = F p.2

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.

theorem LocallyFinite.exists_forall_eventually_atTop_eventually_eq' {X : Type u_4} [] {π : XSort u_6} {f : (x : X) → π x} (hf : LocallyFinite fun (n : ) => {x : X | f (n + 1) x f n x}) :
∃ (F : (x : X) → π x), ∀ (x : X), ∀ᶠ (n : ) in Filter.atTop, ∀ᶠ (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 LocallyFinite.exists_forall_eventually_atTop_eventuallyEq {α : Type u_3} {X : Type u_4} [] {f : Xα} (hf : LocallyFinite fun (n : ) => {x : X | f (n + 1) x f n x}) :
∃ (F : Xα), ∀ (x : X), ∀ᶠ (n : ) in Filter.atTop, 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 LocallyFinite.preimage_continuous {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [] [] {f : ιSet X} {g : YX} (hf : ) (hg : ) :
LocallyFinite fun (x : ι) => g ⁻¹' f x
theorem LocallyFinite.prod_right {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [] [] {f : ιSet X} (hf : ) (g : ιSet Y) :
LocallyFinite fun (i : ι) => f i ×ˢ g i
theorem LocallyFinite.prod_left {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [] [] {g : ιSet Y} (hg : ) (f : ιSet X) :
LocallyFinite fun (i : ι) => f i ×ˢ g i
@[simp]
theorem Equiv.locallyFinite_comp_iff {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [] {f : ιSet X} (e : ι' ι) :
theorem locallyFinite_sum {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [] {f : ι ι'Set X} :
LocallyFinite (f Sum.inl) LocallyFinite (f Sum.inr)
theorem LocallyFinite.sum_elim {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [] {f : ιSet X} {g : ι'Set X} (hf : ) (hg : ) :
theorem locallyFinite_option {ι : Type u_1} {X : Type u_4} [] {f : Set X} :
theorem LocallyFinite.option_elim' {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) (s : Set X) :
theorem LocallyFinite.eventually_subset {ι : Type u_1} {X : Type u_4} [] {s : ιSet X} (hs : ) (hs' : ∀ (i : ι), IsClosed (s i)) (x : X) :
∀ᶠ (y : X) in nhds x, {i : ι | y s i} {i : ι | x s i}