refinement_of_locallyCompact_sigmaCompact_of_nhds_basis
theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis :
∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : WeaklyLocallyCompactSpace X] [inst_2 : SigmaCompactSpace X]
[inst_3 : T2Space X] {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X},
(∀ (x : X), (nhds x).HasBasis (p x) (B x)) →
∃ α c r, (∀ (a : α), p (c a) (r a)) ∧ ⋃ a, B (c a) (r a) = Set.univ ∧ LocallyFinite fun a => B (c a) (r a)
This theorem states that for a locally compact, sigma compact, and Hausdorff topological space `X`, if for every point `x` in `X`, the sets `B x : ι x → Set X`, satisfying the predicate `p x : ι x → Prop`, constitute a basis for the neighborhood filter at `x` (notated as `𝓝 x`), then there exists a locally finite covering of `X` where each cover is of the form `B (c i) (r i)` and each `r i` satisfies `p (c i)`. In essence, this theorem asserts that under these conditions, the space `X` can be covered by locally finite, basis sets that meet certain properties. This theorem has applications in many areas, including the theory of paracompact spaces and smooth manifolds.
More concisely: If a locally compact, sigma compact, and Hausdorff space `X` has a basis of neighborhood filters at each point `x` consisting of sets `B x` satisfying a predicate `p x`, then `X` admits a locally finite covering by sets `B (c i)` with `p (c i)` holding for each cover `B (c i)`.
|
ParacompactSpace.locallyFinite_refinement
theorem ParacompactSpace.locallyFinite_refinement :
∀ {X : Type v} [inst : TopologicalSpace X] [self : ParacompactSpace X] (α : Type v) (s : α → Set X),
(∀ (a : α), IsOpen (s a)) →
⋃ a, s a = Set.univ →
∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
The theorem states that in a paracompact space, every open cover has a locally finite refinement. Specifically, given any topological space which is paracompact and a set of open subsets that covers the whole space, there exists a new set of open subsets, also covering the whole space, such that every point in the space has a neighborhood which intersects with only finitely many of these new subsets and every new subset is contained within one of the original subsets. This is a key property of paracompact spaces in mathematics, particularly in the field of topology.
More concisely: In a paracompact space, every open cover has a locally finite refinement.
|
precise_refinement
theorem precise_refinement :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] [inst_1 : ParacompactSpace X] (u : ι → Set X),
(∀ (a : ι), IsOpen (u a)) →
⋃ i, u i = Set.univ →
∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ i, v i = Set.univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
The theorem `precise_refinement` states that for any open cover of a paracompact space, there exists a locally finite precise refinement. Here, a space is paracompact if every open cover has an open refinement that is locally finite. The open cover is described by a function `u : ι → Set X` where `ι` is an index type and `X` is the space. The theorem ensures that for every index `a : ι`, the set `u a` is open, and the union of all `u i` equals the universal set in `X`. The precise refinement is expressed by a function `v : ι → Set X`, which also satisfies that for every index `a : ι`, `v a` is open, and the union of all `v i` equals the universal set. In addition, this refinement is locally finite, and each set `v a` is a subset of the corresponding set `u_a`, making it a precise refinement.
More concisely: Given a paracompact space X and an open cover u : ι -> Sets X, there exists a locally finite precise refinement v : ι -> Sets X such that for all i in ι, v i is open, u i is the closure of v i, and the union of all v i equals X.
|
precise_refinement_set
theorem precise_refinement_set :
∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] [inst_1 : ParacompactSpace X] {s : Set X},
IsClosed s →
∀ (u : ι → Set X),
(∀ (i : ι), IsOpen (u i)) →
s ⊆ ⋃ i, u i → ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ i, v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
This theorem states that in a paracompact space, every open cover of a closed set can be refined to a locally finite cover, which is indexed by the same type. More specifically, given a paracompact topological space `X` and a closed set `s` in `X`, if there exists an open cover `u` of `s` indexed by type `ι`, the theorem guarantees the existence of an open cover `v` that also indexed by `ι`, such that `v` is a refinement of `u` and is locally finite. This means every point in `X` has a neighborhood that intersects with only finitely many sets in the open cover `v`. Moreover, the set `s` is a subset of the union of all sets in `v`, and each set in `v` is a subset of a corresponding set in `u`.
More concisely: In a paracompact space, every open cover of a closed set can be refined to a locally finite open cover with the same index type, whose union contains the closed set and whose elements are subsets of corresponding sets in the original cover.
|
refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set
theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set :
∀ {X : Type v} [inst : TopologicalSpace X] [inst_1 : WeaklyLocallyCompactSpace X] [inst_2 : SigmaCompactSpace X]
[inst_3 : T2Space X] {ι : X → Type u} {p : (x : X) → ι x → Prop} {B : (x : X) → ι x → Set X} {s : Set X},
IsClosed s →
(∀ x ∈ s, (nhds x).HasBasis (p x) (B x)) →
∃ α c r,
(∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ a, B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
The theorem `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set` states that given a locally compact, sigma compact and Hausdorff topological space `X` and a closed set `s` in `X`, if for every `x` in `s`, the sets `B x : ι x → Set X` under the predicate `p x : ι x → Prop` form a basis of the neighborhood filter of `x`, then there exists a locally finite covering `B (c i) (r i)` of `s` such that all centers `c i` are in `s` and each `r i` satisfies `p (c i)`. This theorem is inspired by metric spaces but can also be applied to other types of spaces, like those with open neighborhoods. The covering can be taken subordinate to some open covering of `s` by using a basis obtained by `Filter.HasBasis.restrict_subset` or similar. This statement is a formalization of two proofs from ncatlab concerning paracompact spaces and smooth manifolds.
More concisely: Given a locally compact, sigma compact, and Hausdorff space `X` with a closed set `s`, if for each `x` in `s`, the sets `B x` under predicate `p x` form a basis for `x`'s neighborhood filter, then there exists a locally finite subordinate covering `B (ci) (ri)` of `s` with `ci` in `s` and `ri` satisfying `p (ci)`.
|