LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo
theorem LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo :
β {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[self : LocallyCompactPair X Y] {f : X β Y} {x : X} {s : Set Y},
Continuous f β s β nhds (f x) β β K β nhds x, IsCompact K β§ Set.MapsTo f K s
This theorem states that considering a pair of topological spaces `X` and `Y` that are locally compact, if there exists a continuous map `f` from `X` to `Y`, and a set `s` in `Y` which is a neighborhood of `f(x)` for some `x` in `X`, then there exists a compact neighborhood `K` of `x` such that the image of `K` under function `f` is contained in `s`. This means that `f` maps every point in `K` to a point in `s`.
More concisely: Given locally compact spaces X and Y, and a continuous function f : X -> Y with image of some x in X contained in a neighborhood s of f(x), there exists a compact neighborhood K of x in X such that the image of K under f is contained in s.
|
WeaklyLocallyCompactSpace.exists_compact_mem_nhds
theorem WeaklyLocallyCompactSpace.exists_compact_mem_nhds :
β {X : Type u_3} [inst : TopologicalSpace X] [self : WeaklyLocallyCompactSpace X] (x : X),
β s, IsCompact s β§ s β nhds x
This theorem states that in a weakly locally compact space, every point has a neighborhood that is a compact set. More specifically, for every point 'x' in a topological space 'X' that is weakly locally compact, there exists a set 's' such that 's' is a compact set and is a neighborhood of 'x'. In the context of topology, a neighborhood of a point is a set that contains an open set around the point, and a space is weakly locally compact if every point has a neighborhood whose closure is compact.
More concisely: In a weakly locally compact topological space, every point has a compact neighborhood.
|
nhds_def
theorem nhds_def :
β {X : Type u_3} [inst : TopologicalSpace X] (x : X), nhds x = β¨
s β {s | x β s β§ IsOpen s}, Filter.principal s
This theorem, `nhds_def`, states that for any type `X` with a topological space structure and any element `x` of `X`, the neighborhood filter of `x` (denoted by `nhds x`) is defined as the infimum (or greatest lower bound) of the set of all principal filters of sets `s` which contain `x` and are open in `X`. In simpler terms, the neighborhood filter of a point in a topological space is a collection of all sets that contain an open set around the point. The theorem provides a precise description of this collection in terms of principal filters, which are filters comprising of all supersets of a given set.
More concisely: The neighborhood filter of a point in a topological space is the infimum of the set of open, principal filters containing that point.
|
NoncompactSpace.noncompact_univ
theorem NoncompactSpace.noncompact_univ :
β {X : Type u_1} [inst : TopologicalSpace X] [self : NoncompactSpace X], Β¬IsCompact Set.univ
This theorem states that in a non-compact topological space, the universal set, which contains all elements of the space, is not a compact set. In other words, for any type `X` equipped with a topological structure and a non-compactness property, it is not the case that every nontrivial filter on `X` that contains the universal set has a cluster point in the universal set. This implies that there must be some filter which cannot be "confined" to a finite subset of the universal set.
More concisely: In a non-compact topological space, the universal set does not have the property of every non-trivial filter containing it having a cluster point in the universal set.
|
CompactSpace.isCompact_univ
theorem CompactSpace.isCompact_univ :
β {X : Type u_1} [inst : TopologicalSpace X] [self : CompactSpace X], IsCompact Set.univ
The theorem `CompactSpace.isCompact_univ` states that in a compact topological space, the universal set is a compact set. In other words, for any given nontrivial filter that contains all elements of the space (since it's the universal set), there exists an element in the space such that every set in the filter intersects every neighborhood of that element. This element is in a sense a "meeting point" for the sets in the filter.
More concisely: In a compact topological space, the universal set is compact and has an element intersecting every neighborhood of any point in it.
|
LocallyCompactSpace.local_compact_nhds
theorem LocallyCompactSpace.local_compact_nhds :
β {X : Type u_3} [inst : TopologicalSpace X] [self : LocallyCompactSpace X] (x : X),
β n β nhds x, β s β nhds x, s β n β§ IsCompact s
In a locally compact space, the theorem `LocallyCompactSpace.local_compact_nhds` states that for every point `x` and any neighborhood `n` of `x`, there exists a compact neighborhood `s` of `x` that is a subset of `n`. In other words, around every point in a locally compact topological space, we can always find a compact neighborhood within any given neighborhood of that point.
More concisely: In every locally compact topological space, for each point and any neighborhood, there exists a compact neighborhood contained in it.
|