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} [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
Instances For
    theorem locallyFinite_of_finite {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] [Finite ι] (f : ιSet X) :
    theorem LocallyFinite.point_finite {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (x : X) :
    {b : ι | x f b}.Finite
    theorem LocallyFinite.subset {ι : Type u_1} {X : Type u_4} [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_2} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} {g : ι'ι} (hf : LocallyFinite f) (hg : Set.InjOn g {i : ι' | (f (g i)).Nonempty}) :
    theorem LocallyFinite.comp_injective {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} {g : ι'ι} (hf : LocallyFinite f) (hg : Function.Injective g) :
    theorem locallyFinite_iff_smallSets {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} :
    LocallyFinite f ∀ (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} [TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (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} [TopologicalSpace X] {f : ιSet X} {ι' : Sort u_6} (hf : LocallyFinite f) {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} [TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (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} [TopologicalSpace X] [TopologicalSpace Y] {f : ιSet X} {g : XY} (hf : LocallyFinite f) (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} [TopologicalSpace X] [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 (⋃ (i : ι), f i)
    theorem LocallyFinite.continuous' {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {f : ιSet X} {g : XY} (hf : LocallyFinite f) (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} [TopologicalSpace X] [TopologicalSpace Y] {f : ιSet X} {g : XY} (hf : LocallyFinite f) (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} [TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) :
    LocallyFinite fun (i : ι) => closure (f i)
    theorem LocallyFinite.closure_iUnion {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} (h : LocallyFinite f) :
    closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
    theorem LocallyFinite.isClosed_iUnion {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (hc : ∀ (i : ι), IsClosed (f i)) :
    IsClosed (⋃ (i : ι), f i)
    theorem LocallyFinite.iInter_compl_mem_nhds {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (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} [TopologicalSpace X] {π : 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} [TopologicalSpace X] {π : 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} [TopologicalSpace X] {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} [TopologicalSpace X] [TopologicalSpace Y] {f : ιSet X} {g : YX} (hf : LocallyFinite f) (hg : Continuous g) :
    LocallyFinite fun (x : ι) => g ⁻¹' f x
    theorem LocallyFinite.prod_right {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {f : ιSet X} (hf : LocallyFinite f) (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} [TopologicalSpace X] [TopologicalSpace Y] {g : ιSet Y} (hg : LocallyFinite g) (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} [TopologicalSpace X] {f : ιSet X} (e : ι' ι) :
    theorem locallyFinite_sum {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [TopologicalSpace X] {f : ι ι'Set X} :
    theorem LocallyFinite.sum_elim {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} {g : ι'Set X} (hf : LocallyFinite f) (hg : LocallyFinite g) :
    theorem locallyFinite_option {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : Option ιSet X} :
    theorem LocallyFinite.option_elim' {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ιSet X} (hf : LocallyFinite f) (s : Set X) :
    theorem LocallyFinite.eventually_subset {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {s : ιSet X} (hs : LocallyFinite s) (hs' : ∀ (i : ι), IsClosed (s i)) (x : X) :
    ∀ᶠ (y : X) in nhds x, {i : ι | y s i} {i : ι | x s i}