locallyCompactSpace_of_hasBasis
theorem locallyCompactSpace_of_hasBasis :
∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : X → Type u_4} {p : (x : X) → ι x → Prop}
{s : (x : X) → ι x → Set X},
(∀ (x : X), (nhds x).HasBasis (p x) (s x)) →
(∀ (x : X) (i : ι x), p x i → IsCompact (s x i)) → LocallyCompactSpace X
The theorem `locallyCompactSpace_of_hasBasis` states that for any type `X` equipped with a topological space structure, given a family of properties `p` and sets `s` indexed by elements of `X` and another type dependent on `X`, if for every `x` in `X`, the neighborhood filter `nhds x` has a basis consisting of sets `s x i` that satisfy the property `p x i`, and for every `x` in `X` and `i` in `ι x` such that `p x i` is true, the set `s x i` is compact, then `X` is a locally compact space. In simpler terms, it provides a condition under which a topological space can be considered locally compact: each point should have a neighborhood basis consisting of compact sets.
More concisely: A topological space `X` is locally compact if for each point `x` in `X`, the neighborhood filter of `x` has a basis of compact sets satisfying property `p` at `x`.
|
exists_mem_nhdsSet_isCompact_mapsTo
theorem exists_mem_nhdsSet_isCompact_mapsTo :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : LocallyCompactPair X Y] {f : X → Y} {K : Set X} {U : Set Y},
Continuous f → IsCompact K → IsOpen U → Set.MapsTo f K U → ∃ L ∈ nhdsSet K, IsCompact L ∧ Set.MapsTo f L U
This theorem states that if we have a continuous map `f` from `X` to `Y` in a locally compact pair of topological spaces, a compact set `K` in `X`, and an open neighbourhood `U` of the image of `K` under `f`, then there exists a compact neighbourhood `L` of `K` such that `f` maps `L` to `U`. This theorem is a generalization of `exists_mem_nhds_isCompact_mapsTo`.
More concisely: Given a continuous map `f` between locally compact spaces `X` and `Y`, a compact set `K` in `X`, and an open set `U` containing `f(K)` in `Y`, there exists a compact neighborhood `L` of `K` in `X` such that `f(L)` is contained in `U`.
|
exists_compact_superset
theorem exists_compact_superset :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : WeaklyLocallyCompactSpace X] {K : Set X},
IsCompact K → ∃ K', IsCompact K' ∧ K ⊆ interior K'
In the mathematical field of topology, this theorem states that in a weakly locally compact space, any compact set is contained within the interior of another compact set. Specifically, for any compact set `K` in a topological space `X` that also has the property of being a weakly locally compact space, there exists another compact set `K'` such that `K` is a subset of the interior of `K'`. Here, the 'interior' of a set refers to the largest open subset of that set. The 'compactness' of a set is a property indicating that for any nontrivial filter containing the set, there exists a point in the set where all sets of the filter meet all neighborhoods of that point. A 'weakly locally compact space' is a specific type of topological space.
More concisely: In a weakly locally compact space, every compact set is contained in the interior of another compact set.
|
compact_basis_nhds
theorem compact_basis_nhds :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyCompactSpace X] (x : X),
(nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsCompact s) fun s => s
The theorem `compact_basis_nhds` states that for any point `x` in a locally compact space `X` (which is a topological space), the neighborhood filter at `x` has a basis where each basis element is both a neighborhood of `x` and a compact set. This means that the neighborhood filter at `x` can be generated by a collection of sets that are both neighborhoods of `x` and compact. This property holds for all points `x` in the space `X`.
More concisely: For every point $x$ in a locally compact space $X$, the neighborhood filter at $x$ has a basis consisting of compact neighborhoods of $x$.
|
local_compact_nhds
theorem local_compact_nhds :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyCompactSpace X] {x : X} {n : Set X},
n ∈ nhds x → ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
The theorem `local_compact_nhds` states that for any given topological space `X` which is locally compact, any point `x` in `X`, and any set `n` that is a neighborhood of `x`, there exists a set `s` which is also a neighborhood of `x`, such that `s` is a subset of `n` and `s` is compact. In other words, in a locally compact topological space, for every neighborhood of every point, we can find a compact neighborhood contained within it.
More concisely: In a locally compact topological space, every neighborhood of a point contains a compact neighborhood of that point.
|
exists_compact_between
theorem exists_compact_between :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyCompactSpace X] {K U : Set X},
IsCompact K → IsOpen U → K ⊆ U → ∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U
The theorem `exists_compact_between` states that in a locally compact space, given a compact set `K` that is a subset of an open set `U`, there exists a compact neighborhood `L` such that `K` is a subset of the interior of `L`, and `L` is a subset of `U`. In other words, for every containment of a compact set `K` within an open set `U`, there is a compact `L` that lies between `K` and `U`. The theorem is also related to `exists_compact_closed_between`, where `L` is additionally guaranteed to be closed if the space is regular.
More concisely: In a locally compact space, for every compact subset `K` of an open set `U`, there exists a compact neighborhood `L` of `K` such that `K` is contained in the interior of `L` and `L` is contained in `U`.
|
LocallyCompactSpace.of_hasBasis
theorem LocallyCompactSpace.of_hasBasis :
∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : X → Type u_4} {p : (x : X) → ι x → Prop}
{s : (x : X) → ι x → Set X},
(∀ (x : X), (nhds x).HasBasis (p x) (s x)) →
(∀ (x : X) (i : ι x), p x i → IsCompact (s x i)) → LocallyCompactSpace X
This theorem, named `LocallyCompactSpace.of_hasBasis`, states that for any type `X` equipped with a topological space structure and a family of sets `s` indexed by a type `ι` that depends on `X` and a predicate `p` on each index, if every neighborhood filter (set of neighborhoods) of each point `x` in `X` has a basis consisting of sets for which the predicate `p` holds and each of these sets is compact, then `X` is a locally compact space.
In simpler terms, it means that if every point in a topological space `X` has a basis of its neighborhoods consisting of compact sets satisfying some property, then `X` itself is a locally compact space. A locally compact space is a topological space where every point has a compact neighborhood.
More concisely: If every point in a topological space `X` has a neighborhood basis consisting of compact sets `s` satisfying predicate `p`, then `X` is a locally compact space.
|
exists_compact_subset
theorem exists_compact_subset :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LocallyCompactSpace X] {x : X} {U : Set X},
IsOpen U → x ∈ U → ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
This theorem states that in a locally compact space, every open set containing a point `x` also contains a compact subset whose interior contains `x`. More precisely, for any topological space `X` that is locally compact, and for any point `x` in `X` and open set `U` containing `x`, there exists a compact set `K` such that `x` is in the interior of `K` and `K` is a subset of `U`.
More concisely: In a locally compact topological space, for each point `x` in an open set `U`, there exists a compact subset `K` of `U` with `x` in the interior of `K`.
|
disjoint_nhds_cocompact
theorem disjoint_nhds_cocompact :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : WeaklyLocallyCompactSpace X] (x : X),
Disjoint (nhds x) (Filter.cocompact X)
This theorem states that, in any weakly locally compact topological space, the neighborhood filter of any point and the filter generated by complements of all compact sets in that space, are disjoint. Here, two filters being disjoint means that the greatest element which is less than or equal to both filters is the bottom element of the lattice structure. In the context of filters, this bottom element typically represents the empty set. So, in essence, the theorem is saying that there is no set that belongs to both the neighborhood filter of a point and the filter of complements of compact sets in a weakly locally compact space.
More concisely: In any weakly locally compact topological space, the neighborhood filter of a point and the filter generated by complements of compact sets are disjoint, implying no set belongs to both filters.
|