LocallyFinite.exists_forall_eventually_eq_prod
theorem LocallyFinite.exists_forall_eventually_eq_prod :
∀ {X : Type u_4} [inst : TopologicalSpace X] {π : X → Sort u_6} {f : ℕ → (x : X) → π x},
(LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) →
∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in Filter.atTop ×ˢ nhds x, f p.1 p.2 = F p.2
This theorem states that, given a sequence of dependent functions `f : ℕ → Π a, β a` on a topological space, if the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite (meaning that for every point in the space, there exists a neighborhood of that point that only intersects finitely many sets in the family), then there exists a function `F : Π a, β a` such that for any point `x` in the space, the functions in the sequence `f` agree with `F` on the product of an infinite interval `[N, +∞)` (moving toward positive infinity) and a neighborhood of `x`. This conclusion is formulated in terms of the product of the filter that represents the limit moving toward infinity (`Filter.atTop`) and the neighborhood filter at `x` (`nhds x`).
More concisely: Given a sequence of dependent functions on a topological space with locally finite sets of points where the functions disagree, there exists a limiting function such that the sequence agrees with it on the product of the filter of points approaching infinity and a neighborhood of any point.
|
LocallyFinite.point_finite
theorem LocallyFinite.point_finite :
∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
LocallyFinite f → ∀ (x : X), {b | x ∈ f b}.Finite
The theorem `LocallyFinite.point_finite` states that for any type `ι`, any type `X` equipped with a topological structure, and any function `f` from `ι` to the set of `X`, if `f` is locally finite - meaning that for every point `x` in `X`, there exists a neighborhood of `x` which intersects only finitely many sets in the family `f` - then for every point `x` in `X`, the set of `b` in `ι` such that `x` belongs to `f b` is finite. In other words, each point in the space `X` belongs to only finitely many sets in the locally finite family `f`.
More concisely: If `f` is a locally finite family of sets over a topological space `X` (i.e., for every point `x` in `X`, there exists a neighborhood of `x` intersecting only finitely many sets in `f`), then for every point `x` in `X`, the set of indices `b` for which `x` belongs to `f(b)` is finite.
|
LocallyFinite.exists_forall_eventually_atTop_eventuallyEq
theorem LocallyFinite.exists_forall_eventually_atTop_eventuallyEq :
∀ {α : Type u_3} {X : Type u_4} [inst : TopologicalSpace X] {f : ℕ → X → α},
(LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) →
∃ F, ∀ (x : X), ∀ᶠ (n : ℕ) in Filter.atTop, (nhds x).EventuallyEq (f n) F
The theorem `LocallyFinite.exists_forall_eventually_atTop_eventuallyEq` states the following:
Given a sequence of functions `f : ℕ → α → β` on a topological space `X`, where `α` and `β` are types, suppose that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite (i.e., for every point `x` in `X`, there is a neighborhood of `x` which intersects with only finitely many sets in the family). Then, there exists a function `F : α → β` such that, for any point `x` in `X`, the function `f n` eventually equals `F` for all sufficiently large `n` (i.e., in the limit as `n` approaches infinity, or `→ ∞`). This is denoted as `f n =ᶠ[𝓝 x] F`, where `=ᶠ[𝓝 x]` indicates "eventually equal" at the neighborhood of `x`.
More concisely: If the family of sets defined by `{x | f (n+1) x != fn x}` is locally finite for a sequence of functions `f : ℕ -> α -> β` on a topological space `X`, then there exists a function `F : α -> β` such that `fn =_ {o x} F` for all `x` in `X`, where `=_ {o x}` indicates eventual equality in the neighborhood of `x`.
|
LocallyFinite.iInter_compl_mem_nhds
theorem LocallyFinite.iInter_compl_mem_nhds :
∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
LocallyFinite f → (∀ (i : ι), IsClosed (f i)) → ∀ (x : X), ⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ nhds x
The theorem `LocallyFinite.iInter_compl_mem_nhds` states that if we have a locally finite family of closed sets `f : β → Set α`, then for any point `x : α`, the intersection of the complements of sets `f i` where `x` is not an element of `f i` forms a neighborhood of `x`. In simpler terms, around any point, we can find a region that avoids infinitely many sets from this family. This is a concept used in topology and the study of topological spaces.
More concisely: Given a locally finite family `f` of closed sets in a topological space `α`, for each point `x ∈ α`, there exists a neighborhood `N` of `x` such that `x` is not in the sets `f i` for all `i` with `f i ∉ N`.
|
LocallyFinite.subset
theorem LocallyFinite.subset :
∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f g : ι → Set X},
LocallyFinite f → (∀ (i : ι), g i ⊆ f i) → LocallyFinite g
The theorem `LocallyFinite.subset` states that for any type `ι` (which is used to index the family of sets), and for any topological space `X`, if we have two families of sets `f` and `g` indexed by type `ι`, with `f` being a locally finite family, and every set in the family `g` is a subset of a corresponding set in the family `f`, then `g` is also a locally finite family. In other words, if a family of sets `f` is locally finite and another family of sets `g` is contained within `f`, then `g` is also locally finite. This is to say, for every point `x` in the topological space, there exist a neighborhood of `x` that intersects with only finitely many sets in the family `g`.
More concisely: If `f` is a locally finite family of sets in a topological space `X` and every set in the family `g` is a subset of some set in `f`, then `g` is also locally finite.
|
LocallyFinite.comp_injective
theorem LocallyFinite.comp_injective :
∀ {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X} {g : ι' → ι},
LocallyFinite f → Function.Injective g → LocallyFinite (f ∘ g)
The theorem `LocallyFinite.comp_injective` states that for any types `ι`, `ι'`, and `X`, where `X` is a topological space, if we have a locally finite family of sets `f : ι → Set X` and an injective function `g : ι' → ι`, then the composition of `f` and `g` (i.e., `f ∘ g`) is also a locally finite family of sets. In other words, under these conditions, if we apply `g` to change the indexing of the sets in the family `f`, the resulting family of sets remains locally finite. This is a statement about the preservation of the property of local finiteness under injective re-indexing.
More concisely: If `f : ι → Sets X` is a locally finite family of sets and `g : ι' → ι` is an injective function, then `f ∘ g` is also a locally finite family of sets.
|
LocallyFinite.exists_forall_eventually_atTop_eventually_eq'
theorem LocallyFinite.exists_forall_eventually_atTop_eventually_eq' :
∀ {X : Type u_4} [inst : TopologicalSpace X] {π : X → Sort u_6} {f : ℕ → (x : X) → π x},
(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
This theorem states that given a sequence of functions `f : ℕ → Π a, β a` on a topological space, if 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 point `x`, for sufficiently large values of `n` (as `n` approaches infinity), the function `f n y` equals `F y` in a neighborhood of `x`.
Here, a family of sets is defined as locally finite if for every point `x`, there is a neighborhood of `x` which intersects with only finitely many sets in the family. The term "eventually" signifies that a particular condition holds for all sufficiently large values.
More concisely: Given a sequence of functions `f : ℕ → Π a, β a` on a topological space with locally finite family of sets `s n = {x | f (n + 1) x neq f n x}`, there exists a function `F : Π a, β a` such that for any point `x`, `f n x` approaches `F x` in a neighborhood of `x` as `n` goes to infinity.
|
LocallyFinite.closure
theorem LocallyFinite.closure :
∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
LocallyFinite f → LocallyFinite fun i => closure (f i)
This theorem states that for any type `ι` and any topological space `X`, if a family of sets `f : ι → Set X` is locally finite, then the family of closures of these sets is also locally finite. In more detail, the function `f` maps elements of type `ι` to sets in `X`, and `LocallyFinite f` means that for every point in `X`, there is a neighborhood of this point that intersects with only a finite number of sets in the family defined by `f`. The theorem claims that this property still holds if each set in the family is replaced by its closure, where the closure of a set is the smallest closed set that contains it.
More concisely: If `f : ι → Sets X` is a locally finite family of sets in a topological space `X`, then the family of closures of `f` is also locally finite.
|