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) : 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.

theorem locallyFinite_of_finite {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] [Finite ι] (f : ι → Set X) : LocallyFinite f

theorem LocallyFinite.point_finite {ι : Type u_1} {X : Type u_4} [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_4} [TopologicalSpace X] {f : ι → Set X} {g : ι → Set X} (hf : LocallyFinite f) (hg : ∀ (i : ι), g i ⊆ f i) : LocallyFinite g

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 | Set.Nonempty (f (g i))}) : LocallyFinite (f ∘ g)

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) : LocallyFinite (f ∘ 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 Filter.smallSets (nhds x), Set.Finite {i | Set.Nonempty (f i ∩ s)}

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 Filter.smallSets (nhds x), Set.Finite {i | Set.Nonempty (f i ∩ s)}

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 : 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} [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 : X → Y} (hf : LocallyFinite f) (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} [TopologicalSpace X] [TopologicalSpace Y] {f : ι → Set X} {g : X → Y} (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 : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ (i : ι), f i = Set.univ) (hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x) : Continuous g

theorem LocallyFinite.continuous {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {f : ι → Set X} {g : X → Y} (hf : LocallyFinite f) (h_cov : ⋃ (i : ι), f i = Set.univ) (h_cl : ∀ (i : ι), IsClosed (f i)) (h_cont : ∀ (i : ι), ContinuousOn g (f i)) : Continuous g

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 : ι) (_ : ¬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} [TopologicalSpace X] {π : X → Sort 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} [TopologicalSpace X] {π : X → Sort 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} [TopologicalSpace X] {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} [TopologicalSpace X] [TopologicalSpace Y] {f : ι → Set X} {g : Y → X} (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 : ι' ≃ ι) : LocallyFinite (f ∘ ↑e) ↔ LocallyFinite f

theorem locallyFinite_sum {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [TopologicalSpace X] {f : ι ⊕ ι' → Set X} : LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)

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) : LocallyFinite (Sum.elim f g)

theorem locallyFinite_option {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : Option ι → Set X} : LocallyFinite f ↔ LocallyFinite (f ∘ some)

theorem LocallyFinite.option_elim' {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ι → Set X} (hf : LocallyFinite f) (s : Set X) : LocallyFinite (Option.elim' s f)