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_2} [inst : TopologicalSpace X] (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
theorem locallyFinite_of_finite {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst : Finite ι] (f : ιSet X) :
theorem LocallyFinite.point_finite {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (x : X) :
Set.Finite { b | x f b }
theorem LocallyFinite.subset {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} {g : ιSet X} (hf : LocallyFinite f) (hg : ∀ (i : ι), g i f i) :
theorem LocallyFinite.comp_injOn {ι : Type u_1} {ι' : Type u_3} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} {g : ι'ι} (hf : LocallyFinite f) (hg : Set.InjOn g { i | Set.Nonempty (f (g i)) }) :
theorem LocallyFinite.comp_injective {ι : Type u_1} {ι' : Type u_3} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} {g : ι'ι} (hf : LocallyFinite f) (hg : Function.Injective g) :
theorem locallyFinite_iff_smallSets {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} :
LocallyFinite f ∀ (x : X), Filter.Eventually (fun s => Set.Finite { i | Set.Nonempty (f i s) }) (Filter.smallSets (nhds x))
theorem LocallyFinite.eventually_smallSets {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (x : X) :
theorem LocallyFinite.exists_mem_basis {ι : Type u_2} {X : Type u_3} [inst : TopologicalSpace X] {f : ιSet X} {ι' : Sort u_1} (hf : LocallyFinite f) {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_unionᵢ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (a : X) :
nhdsWithin a (Set.unionᵢ fun i => f i) = i, nhdsWithin a (f i)
theorem LocallyFinite.continuousOn_unionᵢ' {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst : TopologicalSpace Y] {f : ιSet X} {g : XY} (hf : LocallyFinite f) (hc : ∀ (i : ι) (x : X), x closure (f i)ContinuousWithinAt g (f i) x) :
ContinuousOn g (Set.unionᵢ fun i => f i)
theorem LocallyFinite.continuousOn_unionᵢ {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst : TopologicalSpace Y] {f : ιSet X} {g : XY} (hf : LocallyFinite f) (h_cl : ∀ (i : ι), IsClosed (f i)) (h_cont : ∀ (i : ι), ContinuousOn g (f i)) :
ContinuousOn g (Set.unionᵢ fun i => f i)
theorem LocallyFinite.continuous' {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst : TopologicalSpace Y] {f : ιSet X} {g : XY} (hf : LocallyFinite f) (h_cov : (Set.unionᵢ fun 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_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst : TopologicalSpace Y] {f : ιSet X} {g : XY} (hf : LocallyFinite f) (h_cov : (Set.unionᵢ fun 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_2} [inst : TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) :
LocallyFinite fun i => closure (f i)
theorem LocallyFinite.closure_unionᵢ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} (h : LocallyFinite f) :
closure (Set.unionᵢ fun i => f i) = Set.unionᵢ fun i => closure (f i)
theorem LocallyFinite.isClosed_unionᵢ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (hc : ∀ (i : ι), IsClosed (f i)) :
IsClosed (Set.unionᵢ fun i => f i)
theorem LocallyFinite.interᵢ_compl_mem_nhds {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (hc : ∀ (i : ι), IsClosed (f i)) (x : X) :
(Set.interᵢ fun i => Set.interᵢ fun _hi => 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_2} [inst : TopologicalSpace X] {π : XSort u_1} {f : (x : X) → π x} (hf : LocallyFinite fun n => { x | f (n + 1) x f n x }) :
F, ∀ (x : X), Filter.Eventually (fun p => f p.fst p.snd = F p.snd) (Filter.prod Filter.atTop (nhds 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.

theorem LocallyFinite.exists_forall_eventually_atTop_eventually_eq' {X : Type u_2} [inst : TopologicalSpace X] {π : XSort u_1} {f : (x : X) → π x} (hf : LocallyFinite fun n => { x | f (n + 1) x f n x }) :
F, ∀ (x : X), Filter.Eventually (fun n => Filter.Eventually (fun y => f n y = F y) (nhds x)) Filter.atTop

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_2} {X : Type u_1} [inst : TopologicalSpace X] {f : Xα} (hf : LocallyFinite fun n => { x | f (n + 1) x f n x }) :
F, ∀ (x : X), Filter.Eventually (fun n => f n =ᶠ[nhds x] F) Filter.atTop

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_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst : TopologicalSpace Y] {f : ιSet X} {g : YX} (hf : LocallyFinite f) (hg : Continuous g) :
LocallyFinite fun i => g ⁻¹' f i
@[simp]
theorem Equiv.locallyFinite_comp_iff {ι : Type u_2} {ι' : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {f : ιSet X} (e : ι' ι) :
theorem locallyFinite_sum {ι : Type u_1} {ι' : Type u_2} {X : Type u_3} [inst : TopologicalSpace X] {f : ι ι'Set X} :
theorem LocallyFinite.sum_elim {ι : Type u_2} {ι' : Type u_3} {X : Type u_1} [inst : TopologicalSpace X] {f : ιSet X} {g : ι'Set X} (hf : LocallyFinite f) (hg : LocallyFinite g) :
theorem locallyFinite_option {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : Option ιSet X} :
theorem LocallyFinite.option_elim' {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (s : Set X) :