isSigmaCompact_univ_iff
theorem isSigmaCompact_univ_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X], IsSigmaCompact Set.univ ↔ SigmaCompactSpace X
This theorem states that a topological space is σ-compact if and only if the universal set is σ-compact. In other words, for any topological space 'X', 'X' is said to be σ-compact (meaning it can be represented as a union of countably many compact sets) if and only if the set of all elements of 'X' is also σ-compact.
More concisely: A topological space is σ-compact if and only if its underlying set is σ-compact with respect to the same topology.
|
IsSigmaCompact.image_of_continuousOn
theorem IsSigmaCompact.image_of_continuousOn :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
IsSigmaCompact s → ContinuousOn f s → IsSigmaCompact (f '' s)
This theorem states that if a subset `s` of a topological space `X` is σ-compact, and if a function `f` from `X` to another topological space `Y` is continuous on `s`, then the image of `s` under `f` is also σ-compact. In other words, continuous functions preserve the property of σ-compactness under the operation of image formation. Here, a set is said to be σ-compact if it can be represented as the union of countably many compact subsets.
More concisely: If a σ-compact subset of a topological space is mapped under a continuous function to another topological space, the image is also σ-compact.
|
isSigmaCompact_range
theorem isSigmaCompact_range :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → ∀ [inst : SigmaCompactSpace X], IsSigmaCompact (Set.range f)
The theorem `isSigmaCompact_range` states that if a topological space `X` is sigma-compact (meaning it can be expressed as a countable union of compact subsets) and `f` is a continuous function from `X` to another topological space `Y`, then the image of `f` (denoted by `Set.range f`) is also sigma-compact. This theorem essentially asserts the preservation of sigma-compactness under continuous functions.
More concisely: If `X` is a sigma-compact topological space and `f` is a continuous function from `X` to a topological space `Y`, then the image `Set.range f` is also a sigma-compact subset of `Y`.
|
iUnion_compactCovering
theorem iUnion_compactCovering :
∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X], ⋃ n, compactCovering X n = Set.univ
This theorem states that for any type `X` that has a topology and is a `σ-compact` space (i.e., it can be written as a countable union of compact subsets), the union over all natural numbers `n` of the `compactCovering` of `X` by `n` is equal to the universal set. In other words, every point in the topological space `X` is contained in some compact subset specified by the `compactCovering` function, which is chosen to be monotone. This is a way of saying that the space can be covered entirely by these compact subsets.
More concisely: For any σ-compact topological space X, the union of the first n compact coverings of X for all natural numbers n is equal to X.
|
IsCompact.isSigmaCompact
theorem IsCompact.isSigmaCompact :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsSigmaCompact s
This theorem states that for any given type `X` equipped with a topology, if a set `s` of `X` is compact, then it is also σ-compact. In other words, any compact set can also be expressed as the countable union of compact subsets. In mathematical notation, a set `s` is compact if for every nontrivial filter `f` that contains `s`, there exists an element `a` in `s` such that every set of `f` meets every neighborhood of `a`. A set `s` is σ-compact if it can be written as the countable union of compact sets. The theorem thus establishes that compactness implies σ-compactness in any topological space.
More concisely: In any topological space, every compact set is also σ-compact.
|
IsSigmaCompact.of_isClosed_subset
theorem IsSigmaCompact.of_isClosed_subset :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X},
IsSigmaCompact t → IsClosed s → s ⊆ t → IsSigmaCompact s
The theorem states that for any type `X` equipped with a topological structure, if `t` is a σ-compact subset of `X` and `s` is a closed subset of `X` that is contained within `t`, then `s` is also σ-compact. In other words, a closed subset of a σ-compact set inherits the property of being σ-compact. Here, σ-compactness of a set means that it can be expressed as the union of countably many compact sets.
More concisely: If `t` is a σ-compact subset of a topological space `X` and `s` is a closed subset of `t`, then `s` is also σ-compact.
|
isSigmaCompact_iff_isSigmaCompact_univ
theorem isSigmaCompact_iff_isSigmaCompact_univ :
∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSigmaCompact s ↔ IsSigmaCompact Set.univ
The theorem `isSigmaCompact_iff_isSigmaCompact_univ` states that for any topological space `X` and any subset `s` of `X`, `s` is a sigma-compact set if and only if `s`, considered as a space with the subspace topology, is a sigma-compact space. In other words, a subset of a topological space is sigma-compact (that is, it can be expressed as a countable union of compact sets) if and only if the same set, when seen as a topological space itself, is also sigma-compact.
More concisely: A subset of a topological space is sigma-compact if and only if, viewed as a subspace, it is also a sigma-compact space.
|
isSigmaCompact_biUnion
theorem isSigmaCompact_biUnion :
∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {s : Set ι} {S : ι → Set X},
s.Countable → (∀ i ∈ s, IsSigmaCompact (S i)) → IsSigmaCompact (⋃ i ∈ s, S i)
The theorem `isSigmaCompact_biUnion` states that for any type `X` with a topological space structure and any set `s` of indices of type `ι`, if `s` is countable, and for each index `i` in `s`, the set `S i` (which is a set of elements of type `X`) is σ-compact, then the countable union of all the sets `S i` (for `i` in `s`) is also σ-compact. In other words, countable unions of σ-compact sets preserve σ-compactness in a topological space.
More concisely: If `X` is a topological space and `s` is a countable set of indices such that each `S i` (for `i` in `s`) is σ-compact, then the countable union of all the `S i` is also σ-compact.
|
isSigmaCompact_univ
theorem isSigmaCompact_univ :
∀ {X : Type u_1} [inst : TopologicalSpace X] [h : SigmaCompactSpace X], IsSigmaCompact Set.univ
The theorem `isSigmaCompact_univ` states that in a σ-compact space, the universal set is also σ-compact. Specifically, for any type `X` equipped with a topological space structure, if `X` is a σ-compact space (which means it can be covered by countably many compact subsets), then the universal set of `X` (which contains all elements of `X`) is also σ-compact (i.e., it can also be covered by countably many compact subsets).
More concisely: If a topological space `X` is σ-compact, then its universal set is also σ-compact.
|
isSigmaCompact_iUnion
theorem isSigmaCompact_iUnion :
∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] [inst_1 : Countable ι] (s : ι → Set X),
(∀ (i : ι), IsSigmaCompact (s i)) → IsSigmaCompact (⋃ i, s i)
The theorem `isSigmaCompact_iUnion` states that for any type `X` equipped with a topology and an index type `ι` that is countable, if each set `s i` indexed by `ι` is σ-compact (meaning that it can be expressed as the union of countably many compact sets), then the union of all these `s i` is also σ-compact. In other words, countable unions of σ-compact sets are themselves σ-compact.
More concisely: If `X` is a topological space with a countable index type `ι`, and each set `s i` in the indexed family is σ-compact, then the union of all `s i` is also σ-compact.
|
CompactExhaustion.subset
theorem CompactExhaustion.subset :
∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) ⦃m n : ℕ⦄, m ≤ n → K m ⊆ K n
This theorem states that for any type `X` equipped with a topological space structure and any compact exhaustion `K` of `X`, if you have two natural numbers `m` and `n` such that `m` is less than or equal to `n`, then the `m`th compact subset of `K` is a subset of the `n`th compact subset of `K`. In other words, the compact subsets in a compact exhaustion of a topological space are nested, with each subset being contained within all subsequent subsets in the sequence.
More concisely: For any compact exhaustion `K` of a topological space `X`, the `i`-th compact subset is contained in the `j`-th compact subset for all `i ≤ j`.
|
CompactExhaustion.exists_mem
theorem CompactExhaustion.exists_mem :
∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X), ∃ n, x ∈ K n
This theorem states that for every type `X` that is equipped with a `TopologicalSpace` structure and a `CompactExhaustion` of `X` denoted by `K`, for every element `x` of `X`, there exists an integer `n` such that `x` is an element of `K n`. In other words, given a compact exhaustion `K` of a topological space `X`, any point in `X` is included in one of the compact subsets defined by `K`.
More concisely: For any topological space `(X, top)` with a compact exhaustion `K = {K_n}`, every point `x` in `X` belongs to some `K_n`.
|
SigmaCompactSpace_iff_exists_compact_covering
theorem SigmaCompactSpace_iff_exists_compact_covering :
∀ {X : Type u_1} [inst : TopologicalSpace X],
SigmaCompactSpace X ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ
A topological space is said to be σ-compact if and only if there exists a countable collection of compact subspaces that cover the entire space. In other words, for any type 'X' with the structure of a topological space, 'X' is σ-compact precisely when there is a sequence 'K' of subsets of 'X' such that each 'K n' is compact and the union over all 'n' of the 'K n' equals the entire set 'X'.
More concisely: A topological space X is σ-compact if and only if it can be covered by a countable collection of compact subspaces.
|
countable_cover_nhdsWithin_of_sigma_compact
theorem countable_cover_nhdsWithin_of_sigma_compact :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] {f : X → Set X} {s : Set X},
IsClosed s → (∀ x ∈ s, f x ∈ nhdsWithin x s) → ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
This theorem states that in a sigma-compact topological space, if we have a function `f` that maps each point `x` in a closed set `s` to a neighborhood within `s` of `x`, then there exists a countable subset `t` of `s` such that the neighborhoods `f x` for each `x` in `t` cover the entire set `s`. Sigma-compact means the space is the union of countably many compact subsets. Here, a neighborhood within `s` of `x` refers to the intersection of `s` with a neighborhood of `x`. The countable set `t` and the function `f` together provide a countable coverage of the set `s`.
More concisely: In a sigma-compact topological space, given a closed set and a function mapping each point in the set to a neighborhood of that point within the set, there exists a countable subset covering the entire set whose neighborhoods under the function form a coverage.
|
Subtype.isSigmaCompact_iff
theorem Subtype.isSigmaCompact_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X] {p : X → Prop} {s : Set { a // p a }},
IsSigmaCompact s ↔ IsSigmaCompact (Subtype.val '' s)
This theorem states that for any type `X` with a topological space structure, a predicate `p` on `X`, and a set `s` of elements of the subtype `{a // p a}` (which consists of elements `a` in `X` that satisfy the predicate `p`), `s` is σ-compact if and only if the image of `s` under the subtype value (or coercion) function is σ-compact. In other words, a set of elements that satisfy a certain property is σ-compact if and only if the set of the underlying elements is σ-compact. Here, a set is σ-compact if it can be expressed as the union of countably many compact sets (where compactness is defined in the sense of topology).
More concisely: A subtype of a topological space, defined by a predicate, is σ-compact if and only if its underlying set is σ-compact.
|
Embedding.isSigmaCompact_iff
theorem Embedding.isSigmaCompact_iff :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
Embedding f → (IsSigmaCompact s ↔ IsSigmaCompact (f '' s))
The theorem `Embedding.isSigmaCompact_iff` states that for all types `X` and `Y`, which have topological space structures, and for a function `f` from `X` to `Y`, and a set `s` of type `X`, if the function `f` is an embedding, then the set `s` is σ-compact if and only if the image of the set `s` under the function `f`, denoted as `f '' s`, is σ-compact. In other words, an embedding preserves the σ-compactness property under the image of a set.
In mathematical terms, a set is σ-compact if it can be expressed as a countable union of compact sets. An embedding is a function that is injective and whose image under the function has the same topological properties as the original set.
More concisely: An embedding preserves the σ-compactness property, that is, if an embedding `f: X ⟹ Y` of topological spaces maps a σ-compact set `s ⊆ X` to a σ-compact set `f''s ⊆ Y`.
|
isSigmaCompact_empty
theorem isSigmaCompact_empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsSigmaCompact ∅
The theorem `isSigmaCompact_empty` states that for any type `X` that has a topological space structure, the empty set is σ-compact. In other words, the empty set can be expressed as the union of a countable collection of compact sets.
More concisely: The empty set is a σ-compact subspace of any topological space.
|
isCompact_compactCovering
theorem isCompact_compactCovering :
∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] (n : ℕ),
IsCompact (compactCovering X n)
The theorem `isCompact_compactCovering` states that for every type `X` equipped with a topology and assumed to be a `σ`-compact space (a space that is a countable union of compact subsets), and for every natural number `n`, the `n`-th set in the compact covering of `X` is a compact set. In other words, each set in the sequence of sets that form a monotone choice of compact covering for a `σ`-compact space is itself compact.
More concisely: For any σ-compact space X and every compact covering {C : n in nat}, the n-th set C is compact.
|
countable_cover_nhds_of_sigma_compact
theorem countable_cover_nhds_of_sigma_compact :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] {f : X → Set X},
(∀ (x : X), f x ∈ nhds x) → ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = Set.univ
This theorem states that in a topological space with a sigma compact topology, if we have a function `f` that maps each point `x` to a neighborhood of `x`, then there exists a countable set `s` such that the union of neighborhoods `f(x)`, for each `x` in `s`, covers the entire space. In other words, every point in the space is included in at least one of these neighborhoods. This assertion is an important property in the field of topology, particularly for topological spaces that are sigma compact, which means they can be expressed as a countable union of compact subsets.
More concisely: In a topological space with a sigma compact topology, given a function mapping each point to a neighborhood of that point, there exists a countable subset such that the union of neighborhoods covering the entire space.
|
CompactExhaustion.isCompact'
theorem CompactExhaustion.isCompact' :
∀ {X : Type u_4} [inst : TopologicalSpace X] (self : CompactExhaustion X) (n : ℕ), IsCompact (self.toFun n) := by
sorry
The theorem `CompactExhaustion.isCompact'` states that for any type `X` that has a topological space structure, for any `CompactExhaustion` of `X`, and for any natural number `n`, the function `toFun` applied to `n` gives a set that is compact. In terms of topology, this means that for every nontrivial filter `f` that contains the set returned by `toFun n`, there exists an element in this set such that every set of `f` meets every neighborhood of this element. This concept helps in understanding how compactness can be exhausted or used up in a topological space.
More concisely: For any topological space `(X, τ)` and given a `CompactExhaustion` `{U_i | i < n}` of `X`, the set `{i | i < n ∧ ∃ x ∈ U_i, ∀ V ∈ νx, U_i ∩ V ≠ ∅}` is compact.
|
LocallyFinite.countable_univ
theorem LocallyFinite.countable_univ :
∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] {f : ι → Set X},
LocallyFinite f → (∀ (i : ι), (f i).Nonempty) → Set.univ.Countable
The theorem `LocallyFinite.countable_univ` states that if `X` is a `σ`-compact space (meaning that it is a union of countably many compact subsets), then any locally finite family of non-empty sets in `X` can have only countably many elements. Here, a family of sets is said to be locally finite if at every point `x` in `X`, there exists a neighborhood of `x` that intersects with only finitely many sets in the family. Furthermore, in this context, all sets in the family are non-empty, and the set of all indices labeling the sets in the family is countable.
More concisely: A σ-compact space's locally finite, non-empty family of sets has at most countably many elements.
|
Inducing.isSigmaCompact_iff
theorem Inducing.isSigmaCompact_iff :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
Inducing f → (IsSigmaCompact s ↔ IsSigmaCompact (f '' s))
The theorem `Inducing.isSigmaCompact_iff` states that for any types `X` and `Y` equipped with topological space structures, and for any function `f` from `X` to `Y`, if `f` is inducing, then a set `s` in `X` is σ-compact if and only if its image under `f`, `f '' s`, is σ-compact. In other words, an inducing function preserves the property of being σ-compact under its action. Here, a set is σ-compact if it is the union of countably many compact sets.
More concisely: For any inducing functions between topological spaces, the preimage of a σ-compact set under the function is σ-compact.
|
SigmaCompactSpace.isSigmaCompact_univ
theorem SigmaCompactSpace.isSigmaCompact_univ :
∀ {X : Type u_4} [inst : TopologicalSpace X] [self : SigmaCompactSpace X], IsSigmaCompact Set.univ
This theorem states that in a sigma-compact space, the universal set is a sigma-compact set. In other words, given any type `X` that has a topology and is also a sigma-compact space, the universal set, which contains all elements of `X`, is a sigma-compact set. This implies that the universal set can be represented as the union of countably many compact sets.
More concisely: In a sigma-compact space, the universal set is a sigma-compact set, i.e., it can be expressed as the union of countably many compact sets.
|
CompactExhaustion.subset_interior_succ'
theorem CompactExhaustion.subset_interior_succ' :
∀ {X : Type u_4} [inst : TopologicalSpace X] (self : CompactExhaustion X) (n : ℕ),
self.toFun n ⊆ interior (self.toFun (n + 1))
This theorem states that for any topological space `X` and any compact exhaustion of `X` (which is a sequence of compact subsets that exhausts the space), each subset in the sequence is contained in the interior of the next subset. In other words, if `self` is a compact exhaustion and `n` is a natural number, then the `n`-th subset in the sequence is a subset of the interior of the `(n + 1)`-th subset.
More concisely: For any compact exhaustion `self` of a topological space `X`, the `n`-th compact subset is contained in the interior of the `(n + 1)`-th compact subset for all natural numbers `n`.
|
isSigmaCompact_sUnion
theorem isSigmaCompact_sUnion :
∀ {X : Type u_1} [inst : TopologicalSpace X] (S : Set (Set X)),
S.Countable → (∀ (s : ↑S), IsSigmaCompact ↑s) → IsSigmaCompact S.sUnion
The theorem `isSigmaCompact_sUnion` states that for any type `X` equipped with a topology, if `S` is a set of subsets of `X` which is countable, and every member of `S` is σ-compact (i.e., can be expressed as the union of countably many compact sets), then the union of all the members of `S` is also σ-compact. In other words, the countable union of σ-compact sets is σ-compact. This theorem is part and parcel of the properties of σ-compact sets in a topological space.
More concisely: Given a topological space X and a countable set S of subsets of X, if every set in S is σ-compact, then the union of all sets in S is also σ-compact.
|
IsSigmaCompact.image
theorem IsSigmaCompact.image :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → ∀ {s : Set X}, IsSigmaCompact s → IsSigmaCompact (f '' s)
The theorem `IsSigmaCompact.image` states that if a set `s` in a topological space `X` is sigma-compact and a function `f` from `X` to another topological space `Y` is continuous, then the image of `s` under `f` (denoted as `f(s)`) is also sigma-compact. In other words, the continuity of a function preserves sigma-compactness under the operation of taking images of sets.
More concisely: If `s` is a sigma-compact set in a topological space `X` and `f` is a continuous function from `X` to another topological space `Y`, then `f(s)` is a sigma-compact set in `Y`.
|
CompactExhaustion.mem_find
theorem CompactExhaustion.mem_find :
∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X), x ∈ K (K.find x)
This theorem states that for any type `X` equipped with a topological space structure and any compact exhaustion `K` of `X`, every element `x` of `X` is an element of `K` at the minimal natural number `n` such that `x` is in `K n`. In other words, `x` belongs to the set `K` at the smallest `n` for which it is possible.
More concisely: For any compact exhaustion $K$ of a topological space $X$ and any point $x \in X$, there exists the smallest natural number $n$ such that $x \in K_n$.
|
isSigmaCompact_sUnion_of_isCompact
theorem isSigmaCompact_sUnion_of_isCompact :
∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)},
S.Countable → (∀ s ∈ S, IsCompact s) → IsSigmaCompact S.sUnion
The theorem `isSigmaCompact_sUnion_of_isCompact` states that for any given type `X` with a topological space structure and a set `S` of subsets of `X`, if `S` is countable and every subset `s` in `S` is compact, then the countable union of these compact sets is sigma-compact. In other words, in a topological context, a countable union of compact sets remains sigma-compact.
More concisely: If `X` is a topological space and `S` is a countable collection of compact subsets of `X`, then their countable union is a sigma-compact subset of `X`.
|
compactCovering_subset
theorem compactCovering_subset :
∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] ⦃m n : ℕ⦄,
m ≤ n → compactCovering X m ⊆ compactCovering X n
The theorem `compactCovering_subset` states that for any type `X` equipped with a topology and a sigma-compact space structure, and for any two natural numbers `m` and `n`, if `m` is less than or equal to `n`, then the `m`th set in the compact covering of `X` is a subset of the `n`th set in the compact covering of `X`. This establishes a form of monotonicity for the compact covering of a sigma-compact space.
More concisely: For any sigma-compact space `X` with a topology and a compact covering `{C_i | i < n}`, if `m < n`, then `C_m` is a subset of `C_n`.
|
isSigmaCompact_iUnion_of_isCompact
theorem isSigmaCompact_iUnion_of_isCompact :
∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] [hι : Countable ι] (s : ι → Set X),
(∀ (i : ι), IsCompact (s i)) → IsSigmaCompact (⋃ i, s i)
The theorem `isSigmaCompact_iUnion_of_isCompact` states that for any topological space `X` and any countable index set `ι`, if each `s i` (where `i` is from the index set `ι` and `s : ι → Set X`) is a compact set, then the countable union of these compact sets `s i` is a σ-compact set. Here, a set is compact if for every nontrivial filter that contains the set, there exists an element in the set such that every set of the filter meets every neighborhood of this element. A set is σ-compact if it is the union of countably many compact sets.
More concisely: If every set in a countable family, indexed by an infinite index set, is compact, then their countable union is σ-compact.
|
CompactExhaustion.iUnion_eq'
theorem CompactExhaustion.iUnion_eq' :
∀ {X : Type u_4} [inst : TopologicalSpace X] (self : CompactExhaustion X), ⋃ n, self.toFun n = Set.univ
This theorem states that for any type `X` equipped with a topological space structure and any compact exhaustion of `X`, the union of all sets in this compact exhaustion equals the entire space `X`. In other words, if we take all the sets produced by the compact exhaustion function (which gives us a sequence of compact sets that "exhausts" or covers `X`), and unite them all together, we recover the entire universe of `X`. This is a common property in the study of topological spaces and is particularly useful for understanding the structure of compact subsets.
More concisely: Given a topological space `(X, τ)` and a compact exhaustion `{K_i}`, the union of this exhaustion equals `X`, i.e., `⋃i K_i = X`.
|