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

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) :
Set.Finite {b | x f b}
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 | Set.Nonempty (f (g i))}) :
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 , Set.Finite {i | Set.Nonempty (f i s)}
theorem LocallyFinite.eventually_smallSets {ι : Type u_1} {X : Type u_4} [] {f : ιSet X} (hf : ) (x : X) :
∀ᶠ (s : Set X) in , Set.Finite {i | Set.Nonempty (f i s)}
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 : Filter.HasBasis (nhds x) p s) :
i, p i Set.Finite {j | Set.Nonempty (f j s i)}
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 : ι) (x : X), x closure (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 : ι) (x : X), x closure (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 : ι) (_ : ¬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 LocallyFinite.exists_forall_eventually_eq_prod {X : Type u_4} [] {π : XSort u_6} {f : (x : X) → π x} (hf : LocallyFinite fun n => {x | f (n + 1) x f n x}) :
F, ∀ (x : X), ∀ᶠ (p : × X) in Filter.atTop ×ˢ nhds x, 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.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 | f (n + 1) x f n x}) :
F, ∀ (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 | f (n + 1) x f n x}) :
F, ∀ (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) :