mathlib3documentation

topology.locally_finite

Locally finite families of sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 locally_finite {ι : Type u} {X : Type u_3} (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.

Equations
theorem locally_finite_of_finite {ι : Type u} {X : Type u_3} [finite ι] (f : ι set X) :
theorem locally_finite.point_finite {ι : Type u} {X : Type u_3} {f : ι set X} (hf : locally_finite f) (x : X) :
{b : ι | x f b}.finite
@[protected]
theorem locally_finite.subset {ι : Type u} {X : Type u_3} {f g : ι set X} (hf : locally_finite f) (hg : (i : ι), g i f i) :
theorem locally_finite.comp_inj_on {ι : Type u} {ι' : Type u_1} {X : Type u_3} {f : ι set X} {g : ι' ι} (hf : locally_finite f) (hg : {i : ι' | (f (g i)).nonempty}) :
theorem locally_finite.comp_injective {ι : Type u} {ι' : Type u_1} {X : Type u_3} {f : ι set X} {g : ι' ι} (hf : locally_finite f) (hg : function.injective g) :
theorem locally_finite_iff_small_sets {ι : Type u} {X : Type u_3} {f : ι set X} :
(x : X), ∀ᶠ (s : set X) in (nhds x).small_sets, {i : ι | (f i s).nonempty}.finite
@[protected]
theorem locally_finite.eventually_small_sets {ι : Type u} {X : Type u_3} {f : ι set X} (hf : locally_finite f) (x : X) :
∀ᶠ (s : set X) in (nhds x).small_sets, {i : ι | (f i s).nonempty}.finite
theorem locally_finite.exists_mem_basis {ι : Type u} {X : Type u_3} {f : ι set X} {ι' : Sort u_1} (hf : locally_finite f) {p : ι' Prop} {s : ι' set X} {x : X} (hb : (nhds x).has_basis p s) :
(i : ι') (hi : p i), {j : ι | (f j s i).nonempty}.finite
@[protected]
theorem locally_finite.nhds_within_Union {ι : Type u} {X : Type u_3} {f : ι set X} (hf : locally_finite f) (a : X) :
( (i : ι), f i) = (i : ι), (f i)
theorem locally_finite.continuous_on_Union' {ι : Type u} {X : Type u_3} {Y : Type u_4} {f : ι set X} {g : X Y} (hf : locally_finite f) (hc : (i : ι) (x : X), x closure (f i) (f i) x) :
( (i : ι), f i)
theorem locally_finite.continuous_on_Union {ι : Type u} {X : Type u_3} {Y : Type u_4} {f : ι set X} {g : X Y} (hf : locally_finite f) (h_cl : (i : ι), is_closed (f i)) (h_cont : (i : ι), (f i)) :
( (i : ι), f i)
@[protected]
theorem locally_finite.continuous' {ι : Type u} {X : Type u_3} {Y : Type u_4} {f : ι set X} {g : X Y} (hf : locally_finite f) (h_cov : ( (i : ι), f i) = set.univ) (hc : (i : ι) (x : X), x closure (f i) (f i) x) :
@[protected]
theorem locally_finite.continuous {ι : Type u} {X : Type u_3} {Y : Type u_4} {f : ι set X} {g : X Y} (hf : locally_finite f) (h_cov : ( (i : ι), f i) = set.univ) (h_cl : (i : ι), is_closed (f i)) (h_cont : (i : ι), (f i)) :
@[protected]
theorem locally_finite.closure {ι : Type u} {X : Type u_3} {f : ι set X} (hf : locally_finite f) :
locally_finite (λ (i : ι), closure (f i))
theorem locally_finite.closure_Union {ι : Type u} {X : Type u_3} {f : ι set X} (h : locally_finite f) :
closure ( (i : ι), f i) = (i : ι), closure (f i)
theorem locally_finite.is_closed_Union {ι : Type u} {X : Type u_3} {f : ι set X} (hf : locally_finite f) (hc : (i : ι), is_closed (f i)) :
is_closed ( (i : ι), f i)
theorem locally_finite.Inter_compl_mem_nhds {ι : Type u} {X : Type u_3} {f : ι set X} (hf : locally_finite f) (hc : (i : ι), is_closed (f i)) (x : X) :
( (i : ι) (hi : 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 locally_finite.exists_forall_eventually_eq_prod {X : Type u_3} {π : X Sort u_1} {f : Π (x : X), π x} (hf : locally_finite (λ (n : ), {x : X | f (n + 1) x f n x})) :
(F : Π (x : X), π x), (x : X), ∀ᶠ (p : × X) in , 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.at_top and 𝓝 x.

theorem locally_finite.exists_forall_eventually_at_top_eventually_eq' {X : Type u_3} {π : X Sort u_1} {f : Π (x : X), π x} (hf : locally_finite (λ (n : ), {x : X | f (n + 1) x f n x})) :
(F : Π (x : X), π x), (x : X), ∀ᶠ (n : ) in filter.at_top, ∀ᶠ (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 locally_finite.exists_forall_eventually_at_top_eventually_eq {α : Type u_2} {X : Type u_3} {f : X α} (hf : locally_finite (λ (n : ), {x : X | f (n + 1) x f n x})) :
(F : X α), (x : X), ∀ᶠ (n : ) in filter.at_top, 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 locally_finite.preimage_continuous {ι : Type u} {X : Type u_3} {Y : Type u_4} {f : ι set X} {g : Y X} (hf : locally_finite f) (hg : continuous g) :
locally_finite (λ (i : ι), g ⁻¹' f i)
@[simp]
theorem equiv.locally_finite_comp_iff {ι : Type u} {ι' : Type u_1} {X : Type u_3} {f : ι set X} (e : ι' ι) :
theorem locally_finite_sum {ι : Type u} {ι' : Type u_1} {X : Type u_3} {f : ι ι' set X} :
theorem locally_finite.sum_elim {ι : Type u} {ι' : Type u_1} {X : Type u_3} {f : ι set X} {g : ι' set X} (hf : locally_finite f) (hg : locally_finite g) :
theorem locally_finite_option {ι : Type u} {X : Type u_3} {f : set X} :
theorem locally_finite.option_elim {ι : Type u} {X : Type u_3} {f : ι set X} (hf : locally_finite f) (s : set X) :