IsCompact.image_of_continuousOn
theorem IsCompact.image_of_continuousOn :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
IsCompact s → ContinuousOn f s → IsCompact (f '' s)
The theorem `IsCompact.image_of_continuousOn` states that for any topological spaces `X` and `Y`, a set `s` in `X`, and a function `f` from `X` to `Y`, if the set `s` is compact and the function `f` is continuous on the set `s`, then the image of the set `s` under the function `f` (denoted by `f '' s`) is also compact. In mathematical terms, this can be written as: if a function is continuous on a compact set, then the image of that set under the function is also compact.
More concisely: If a compact set is mapped by a continuous function, the image is also a compact set.
|
IsCompact.union
theorem IsCompact.union :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsCompact t → IsCompact (s ∪ t)
This theorem states that if we have two sets, `s` and `t`, in a topological space `X`, and both `s` and `t` are compact, then their union is also compact. In mathematical terms, if `s` and `t` are subsets of a topological space `X` such that for any nontrivial filter `f` that contains `s` or `t`, there exists an element in `s` or `t` such that every set of `f` meets every neighborhood of that element, then the same property holds for the union of `s` and `t`.
More concisely: If `s` and `t` are compact subsets of a topological space `X`, then their union `s ∪ t` is also compact.
|
isCompact_pi_infinite
theorem isCompact_pi_infinite :
∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)},
(∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}
**Tychonoff's Theorem**: For any index set `ι`, and for any function `X` that maps each index `i` to a topological space `(X i)`, if each `s i` is a compact set in its respective topological space, then the product set `{x | ∀ (i : ι), x i ∈ s i}` is also a compact set. In other words, the product of compact sets is compact. This theorem is a cornerstone of infinite product topology.
More concisely: For any index set ι and family (Xi : Top) of compact spaces, the product space ∏i : ι, Xi carries the product topology and is compact.
|
Ultrafilter.le_nhds_lim
theorem Ultrafilter.le_nhds_lim :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (F : Ultrafilter X), ↑F ≤ nhds F.lim := by
sorry
This theorem states that for any type `X` with a topological space structure and a compact space structure, and for any ultrafilter `F` on `X`, the ultrafilter `F` is less than or equal to the neighborhood filter at the limit of `F`. In other words, every set in the ultrafilter `F` is also in the neighborhood filter at the limit of `F`. Note that the limit of an ultrafilter, if it exists, is a certain element of the underlying type `X`.
More concisely: For any compact topological space `(X, τ)` and an ultrafilter `F` on `X`, the ultrafilter `F` is contained in the neighborhood filter of the limit of `F`.
|
Inducing.isCompact_iff
theorem Inducing.isCompact_iff :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
Inducing f → (IsCompact s ↔ IsCompact (f '' s))
The theorem `Inducing.isCompact_iff` states that for any two types `X` and `Y` with given topological spaces, a set `s` of type `X`, and a function `f` from `X` to `Y`, if `f` is an inducing function, then the set `s` is compact if and only if the image of `s` under `f` (denoted as `f '' s`) is compact.
Here, a set is said to be compact if for any nontrivial filter that contains the set, there exists an element within the set such that every set in the filter intersects every neighborhood of that element. An inducing function is one that induced the topology of the function's codomain on its domain.
More concisely: If `f` is an inducing function from a compact set `s` in type `X` to `Y`, then the image `f '' s` is a compact set in `Y`.
|
IsCompact.compl_mem_sets_of_nhdsWithin
theorem IsCompact.compl_mem_sets_of_nhdsWithin :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s → ∀ {f : Filter X}, (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, tᶜ ∈ f) → sᶜ ∈ f
The theorem `IsCompact.compl_mem_sets_of_nhdsWithin` states that for any type `X` equipped with a topology and any set `s` in `X`, if `s` is compact, then the complement of `s` belongs to a filter `f` given that each element `x` in `s` has a neighborhood `t` within `s` such that the complement of `t` belongs to `f`. In other words, if we have a compact set and for each point in this set there exists a neighborhood of the point, such that the outside of this neighborhood is in a filter, then the outside of the set itself is also in the filter.
More concisely: If `X` is a topological space, `s` is a compact subset of `X`, and for each `x` in `s`, there exists a neighborhood `t` of `x` in `s` such that the complement of `t` is in a filter `f`, then the complement of `s` is in `f`.
|
Filter.cocompact_eq_cofinite
theorem Filter.cocompact_eq_cofinite :
∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : DiscreteTopology X], Filter.cocompact X = Filter.cofinite
This theorem states that for any type `X`, given a topological space structure and a discrete topology on `X`, the filter generated by complements to compact sets in `X` (`Filter.cocompact X`) is equal to the cofinite filter (`Filter.cofinite`). The cofinite filter is the filter of subsets whose complements are finite. This means in such a discrete topological space, the complements of compact sets form a collection of sets where each complement set is finite.
More concisely: In a discrete topological space, the filter of complements to compact sets is equal to the cofinite filter.
|
Filter.hasBasis_coclosedCompact
theorem Filter.hasBasis_coclosedCompact :
∀ {X : Type u} [inst : TopologicalSpace X],
(Filter.coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl
This theorem states that for any type `X` with a topological space structure, the filter `Filter.coclosedCompact X` has a basis. The basis consists of the complements of sets that satisfy two conditions: the set is closed and the set is compact. In other words, given any element in the `Filter.coclosedCompact X`, we can find a closed and compact set whose complement is contained in the original element. This is important as it provides a way to understand and manipulate elements of the `Filter.coclosedCompact` in terms of more easily-understood closed and compact sets.
More concisely: The filter of coclosed and compact sets in a topological space has a basis consisting of closed and compact sets.
|
tendsto_nhds_of_unique_mapClusterPt
theorem tendsto_nhds_of_unique_mapClusterPt :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] {l : Filter Y} {y : X}
{f : Y → X}, (∀ (x : X), MapClusterPt x l f → x = y) → Filter.Tendsto f l (nhds y)
The theorem `tendsto_nhds_of_unique_mapClusterPt` states that: Given a function `f` from a set `Y` to a compact topological space `X`, and a filter `l` on `Y`, if `y` in `X` is a unique cluster point of `f` mapped along `l` (meaning, for every point `x` in `X`, `x` is a cluster point of `f` mapped along `l` if and only if `x` equals `y`), then `f` tends to the neighborhood of `y` along `l`. In other words, for every neighborhood of `y`, the pre-image of this neighborhood under `f` is a neighborhood in the filter `l`, implying that the function `f` gets arbitrarily close to `y` when the arguments get sufficiently close to the elements determining the filter `l`.
More concisely: Given a compact space X, a function f from Y to X, and a filter l on Y such that f maps l to a singleton set {y} in X, then f tends to the neighborhood of y along l.
|
noncompact_univ
theorem noncompact_univ :
∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : NoncompactSpace X], ¬IsCompact Set.univ
This theorem states that for any type `X` equipped with a topological space structure, if `X` is a noncompact space, then the universal set of `X` (that is, the set of all elements of `X`) is not compact. In more mathematical terms, this means that there doesn't exist an element in the universal set such that every set from any nontrivial filter on `X` that contains the universal set intersects every neighborhood of that element.
More concisely: If `X` is a noncompact topological space, then its universal set has no compact element intersecting every neighborhood in every nontrivial filter on `X`.
|
IsCompact.of_isClosed_subset
theorem IsCompact.of_isClosed_subset :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsClosed t → t ⊆ s → IsCompact t
This theorem states that a closed subset of a compact set is also a compact set. More specifically, given any type `X` with a topological space structure, and any two sets `s` and `t` of type `X`, if `s` is compact, `t` is closed, and `t` is a subset of `s`, then `t` is also compact. In mathematical terms, it encapsulates the property that compactness is hereditary with respect to taking closed subsets within topological spaces.
More concisely: If a closed subset of a compact topological space is compact.
|
ClosedEmbedding.noncompactSpace
theorem ClosedEmbedding.noncompactSpace :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : NoncompactSpace X]
{f : X → Y}, ClosedEmbedding f → NoncompactSpace Y
This theorem states that if we have two types `X` and `Y` which are equipped with topological space structures and `X` is a noncompact space, then for any function `f` from `X` to `Y`, if `f` is a closed embedding, it follows that `Y` is also a noncompact space. This essentially implies that a closed embedding from a noncompact space to another space preserves the noncompactness of the domain.
More concisely: If `X` is a noncompact topological space and `f : X → Y` is a closed embedding, then `Y` is also a noncompact topological space.
|
IsClosed.isCompact
theorem IsClosed.isCompact :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [inst_1 : CompactSpace X], IsClosed s → IsCompact s := by
sorry
This theorem states that for any type `X` which has a topological space structure and a set `s` of `X` elements, if `X` has a compact space structure and the set `s` is closed, then the set `s` is also compact. Compactness here is defined in terms of filters: a set is compact if for any nontrivial filter that contains the set, there exists an element in the set such that every set of the filter intersects every neighborhood of that element.
More concisely: If `X` is a compact topological space and `s` is a closed subset of `X`, then `s` is compact.
|
IsCompact.inter_left
theorem IsCompact.inter_left :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact t → IsClosed s → IsCompact (s ∩ t)
The theorem states that in a given topological space, if we have a compact set and a closed set, the intersection of the two sets is also a compact set. Here, a compact set is defined such that 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 that element. A set is closed if it contains all its limit points.
More concisely: In a topological space, the intersection of a compact and closed set is a compact set.
|
isCompact_empty
theorem isCompact_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsCompact ∅
The theorem `isCompact_empty` states that for any type `X` with a topology (that is, `X` is a topological space), the empty set in `X` is compact. In other words, if you take any nontrivial filter `f` that contains the empty set, there will always exist a point in the empty set such that every set of `f` intersects every neighborhood of that point. However, since the empty set has no elements, this condition is vacuously true.
More concisely: The empty set in a topological space is compact.
|
isCompact_of_finite_subcover
theorem isCompact_of_finite_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
(∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i) →
IsCompact s
This theorem states that a set `s` is compact in a given topological space, if for every open cover of `s`, there exists a finite subcover. In other words, if for any collection of open sets `U` indexed by `ι` (where each `U i` is an open set) that covers `s` (i.e., `s` is a subset of the union of these open sets), there exists a finite index set `t` such that `s` is also a subset of the union of the `U i` for `i` in `t`, then `s` is a compact set. This is a common formulation of compactness in topology, and one of its main uses is in proving the Heine-Borel theorem.
More concisely: A set is compact in a topological space if every open cover has a finite subcover.
|
Filter.coprodᵢ_cocompact
theorem Filter.coprodᵢ_cocompact :
∀ {ι : Type u_1} {X : ι → Type u_3} [inst : (d : ι) → TopologicalSpace (X d)],
(Filter.coprodᵢ fun d => Filter.cocompact (X d)) = Filter.cocompact ((d : ι) → X d)
Tychonoff's theorem is expressed in terms of filters in this theorem. It states that for any indexed type `ι` and a function `X` that maps each element of type `ι` to a topological space, the coproduct filter (`Filter.coprodᵢ`) of the filters generated by complements of compact sets (`Filter.cocompact`) on each `X d` is equal to the filter generated by complements of compact sets on the indexed product type `(d : ι) → X d`. In other words, the theorem connects the concept of compact sets in the individual spaces `X d` with the concept of compact sets in the product space `(d : ι) → X d`.
More concisely: The coproduct filter of the complements of compact sets on the spaces `X d` for an indexed type `ι` is equal to the filter of complements of compact sets on the product space `(d : ι) → X d`.
|
isCompact_univ_pi
theorem isCompact_univ_pi :
∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)},
(∀ (i : ι), IsCompact (s i)) → IsCompact (Set.univ.pi s)
**Tychonoff's theorem**: Given an index set `ι` and a family of types `X` indexed by `ι`, where each type `X i` has a topology, if for each `i` in `ι`, the set `s i` in `X i` is compact, then the product set, which consists of all possible functions `f` such that `f i` belongs to `s i` for all `i` in `ι`, is also compact. Here, a set is said to be compact if for any nontrivial filter on it, there exists an element in the set such that every set in the filter meets every neighborhood of the element.
More concisely: Given a family of compact sets `{Si : i ∈ I}` in topological spaces indexed by a set `I`, the product space carries the product topology and is compact.
|
exists_subset_nhds_of_isCompact'
theorem exists_subset_nhds_of_isCompact' :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] [inst_1 : Nonempty ι] {V : ι → Set X},
Directed (fun x x_1 => x ⊇ x_1) V →
(∀ (i : ι), IsCompact (V i)) →
(∀ (i : ι), IsClosed (V i)) → ∀ {U : Set X}, (∀ x ∈ ⋂ i, V i, U ∈ nhds x) → ∃ i, V i ⊆ U
The theorem `exists_subset_nhds_of_isCompact'` states that for any topological space `X` and for any index set `ι`, if `V : ι → Set X` is a decreasing family of closed, compact subsets of `X`, then for any neighborhood `U` of the intersection of the family `V` (denoted as `⋂ i, V i`), there exists an index `i` such that `V i` is a subset of `U`. In other words, any neighborhood of the intersection of a sequence of decreasing compact closed sets must contain at least one of these sets. It is important to note that each set `V i` is assumed to be compact and closed since the space `X` is not necessarily Hausdorff (a condition in which any two distinct points can be separated by neighborhoods).
More concisely: Given a topological space X and an index set ι, if V is a decreasing family of closed and compact subsets of X, then for any neighborhood U of their intersection, there exists an i in ι such that Vi ⊆ U.
|
finite_of_compact_of_discrete
theorem finite_of_compact_of_discrete :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst : DiscreteTopology X], Finite X := by
sorry
This theorem states that a compact discrete space is finite. In other words, for any type `X` which has a topological space structure, if `X` is both a compact space and a discrete space, then `X` is finite. The mathematical implications of this are that no infinite set can be both compact and discrete, which is a fundamental property in topology.
More concisely: A compact discrete space is a finite set.
|
IsCompact.nhdsSet_prod_eq
theorem IsCompact.nhdsSet_prod_eq :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
IsCompact s → IsCompact t → nhdsSet (s ×ˢ t) = nhdsSet s ×ˢ nhdsSet t
The theorem `IsCompact.nhdsSet_prod_eq` states that in the context of topological spaces, if `s` and `t` are compact sets, then the neighborhood filter of the Cartesian product set `s ×ˢ t` equals the Cartesian product of the individual neighborhood filters for `s` and `t`. In less formal terms, this theorem is asserting that the neighborhoods around a pair of points in the Cartesian product of two compact sets can be described in terms of the neighborhoods around the individual points in the respective sets. For general sets, this strict equality may not hold, but the neighborhood filter of the product set is always at least as big as the product of the individual neighborhood filters, as indicated by the theorem `nhdsSet_prod_le`.
More concisely: In the context of topological spaces, if `s` and `t` are compact sets, then the neighborhood filter of their Cartesian product `s ×ˢ t` equals the neighborhood filter of `s ×ˢ t` being the product of the neighborhood filters of `s` and `t` (i.e., `nhds(s ×ˢ t) = nhds(s) ×ˢ nhds(t)`).
|
isCompact_iff_compactSpace
theorem isCompact_iff_compactSpace :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s ↔ CompactSpace ↑s
The theorem `isCompact_iff_compactSpace` states that for any type `X` endowed with a topological space structure and any set `s` of type `X`, the set `s` is compact if and only if the set `s` considered as a type has a structure of compact space. Here, compactness of a set is defined such that for every nontrivial filter `f` that contains the set, there exists an element in the set such that every set of the filter intersects every neighborhood of this element. A compact space is a space where every open cover has a finite subcover.
More concisely: A set in a topological space is compact if and only if it has the structure of a compact space, where a compact space is a space such that every open cover has a finite subcover.
|
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
theorem IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed :
∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type v} [hι : Nonempty ι] (t : ι → Set X),
Directed (fun x x_1 => x ⊇ x_1) t →
(∀ (i : ι), (t i).Nonempty) →
(∀ (i : ι), IsCompact (t i)) → (∀ (i : ι), IsClosed (t i)) → (⋂ i, t i).Nonempty
Cantor's Intersection Theorem states that for a given directed family of nonempty, compact, and closed sets in a topological space, the intersection of all these sets is also nonempty.
In more detail, suppose we have a type `X` equipped with a topology, another type `ι` (which is not empty), and a function `t` that maps `ι` to sets of `X`. If the family of sets defined by `t` is directed by the subset relation (meaning that for any pair of sets in the family, there exists another set in the family that contains both), each of these sets is nonempty, each set is compact (meaning any nontrivial filter containing it has a cluster point in it), and each set is closed (in the topological sense), then the intersection over all these sets (represented by `(⋂ i, t i)`) is also nonempty.
More concisely: Given a nonempty directed family of compact and closed sets in a topological space, their intersection is nonempty.
|
le_nhds_of_unique_clusterPt
theorem le_nhds_of_unique_clusterPt :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] {l : Filter X} {y : X},
(∀ (x : X), ClusterPt x l → x = y) → l ≤ nhds y
This theorem states that in a compact topological space, if a filter has a unique cluster point `y`, then the filter is less than or equal to the neighborhood filter of `y`. In other words, if a particular point `y` is the only cluster point of a filter in a compact topological space, then all elements of the filter are also elements of the neighborhood of `y`.
More concisely: In a compact topological space, a filter having a unique cluster point `y` is contained in the neighborhood filter of `y`.
|
generalized_tube_lemma
theorem generalized_tube_lemma :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X},
IsCompact s →
∀ {t : Set Y},
IsCompact t →
∀ {n : Set (X × Y)}, IsOpen n → s ×ˢ t ⊆ n → ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
The `generalized_tube_lemma` states that given any two compact sets `s` and `t` in topological spaces `X` and `Y` respectively, and an open neighborhood `n` of the Cartesian product of `s` and `t`, there exist open neighborhoods `u` and `v` of `s` and `t` respectively such that the Cartesian product of `u` and `v` is a subset of `n`. In mathematical terms, if `s ⊂ X` and `t ⊂ Y` are compact and `n ⊂ X × Y` is open and contains `s × t`, then there exist open sets `u ⊂ X` and `v ⊂ Y` with `s ⊂ u`, `t ⊂ v`, and `u × v ⊂ n`.
More concisely: Given compact sets `s` in `X` and `t` in `Y`, and an open neighborhood `n` of `s × t` in `X × Y`, there exist open neighborhoods `u` of `s` in `X` and `v` of `t` in `Y` such that `u × v` is a subset of `n`.
|
IsCompact.inter_iInter_nonempty
theorem IsCompact.inter_iInter_nonempty :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
IsCompact s →
∀ (t : ι → Set X),
(∀ (i : ι), IsClosed (t i)) → (∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty) → (s ∩ ⋂ i, t i).Nonempty
The theorem `IsCompact.inter_iInter_nonempty` states that for a given compact set `s` in a topological space `X` and a family of closed sets `t` indexed by `ι`, if `s` intersects with every finite subfamily of `t`, then `s` also intersects with the intersection of the entire family of `t`. In other words, if `s` has a nonempty intersection with every finite intersection of sets in `t`, then `s` has a nonempty intersection with the intersection of all sets in `t`. This theorem is a key result in the theory of compactness in topology, highlighting the "finite intersection" property of compact sets.
More concisely: If a compact set intersects every finite subcollection of a family of closed sets, then it intersects the intersection of the entire family.
|
IsCompact.induction_on
theorem IsCompact.induction_on :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s →
∀ {p : Set X → Prop},
p ∅ →
(∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) →
(∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)) → (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) → p s
The theorem `IsCompact.induction_on` states that for a given topological space `X` and a compact set `s` in `X`, if a property `p` holds for the empty set, is preserved under set restriction (i.e., if `s` is a subset of `t` and `p` holds for `t`, then `p` holds for `s`) and union, and for every point `x` in set `s` there exists a neighborhood `t` within `s` such that property `p` holds for `t`, then property `p` holds for the set `s` itself. This theorem serves as an induction principle for compact sets in a topological space.
More concisely: If a property is empty-cases, union-preserving, and satisfies the finite intersection property on the open neighborhoods of each point in a compact set, then it holds for the set itself.
|
Inducing.isCompact_preimage
theorem Inducing.isCompact_preimage :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Inducing f → IsClosed (Set.range f) → ∀ {K : Set Y}, IsCompact K → IsCompact (f ⁻¹' K)
The theorem "Inducing.isCompact_preimage" asserts that for any two types `X` and `Y` with topological space structures, if a function `f` from `X` to `Y` is inducing and the range of `f` is closed, then the preimage of a compact set `K` in `Y` under `f` is also compact in `X`. In other words, if we have a function that preserves the topology, and for any compact set in the codomain, its preimage under this function is also compact in the domain.
More concisely: If `f` is a continuous function from a topological space `X` to a topological space `Y` with `f` inducing and the range of `f` being closed, then the preimage of any compact set in `Y` under `f` is compact in `X`.
|
Filter.hasBasis_cocompact
theorem Filter.hasBasis_cocompact :
∀ {X : Type u} [inst : TopologicalSpace X], (Filter.cocompact X).HasBasis IsCompact compl
The theorem `Filter.hasBasis_cocompact` asserts that for any type `X` equipped with a topological space structure, the filter `cocompact X`, which is generated by the complements of compact sets, has a basis given by the collection of complements of compact sets. In other words, every set in the `cocompact X` filter can be written as a union of complements of compact sets, and for every complement of a compact set, there is a set in the `cocompact X` filter that contains it.
More concisely: The filter generated by the complements of compact sets in a topological space has a basis consisting of complements of compact sets.
|
cluster_point_of_compact
theorem cluster_point_of_compact :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (f : Filter X) [inst_2 : f.NeBot],
∃ x, ClusterPt x f
This theorem, named `cluster_point_of_compact`, asserts that for all topological spaces `X` that are also compact, given a filter `f` on `X` that is not the bottom filter, there exists a point `x` in `X` that is a cluster point of the filter `f`. In mathematical terms, this states that every non-trivial filter on a compact topological space has a cluster point.
More concisely: Every non-trivial filter on a compact topological space has a cluster point.
|
IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed
theorem IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type v} [hι : Nonempty ι] (t : ι → Set X),
Directed (fun x x_1 => x ⊇ x_1) t →
(∀ (i : ι), (t i).Nonempty) →
(∀ (i : ι), IsCompact (t i)) → (∀ (i : ι), IsClosed (t i)) → (⋂ i, t i).Nonempty
The theorem `IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed` is a version of Cantor's intersection theorem for the intersection (`iInter`) operation in Lean. Specifically, it states that for any topological space `X` and any type `ι` (assumed nonempty), if `t` is a function from `ι` into the sets of `X` such that `t` is directed under set inclusion, every set `t i` is nonempty, every set `t i` is compact and every set `t i` is closed, then the intersection of all sets `t i` (denoted `(⋂ i, t i)`) is nonempty. In other words, the intersection of a directed family of nonempty compact closed sets in a topological space is nonempty.
More concisely: Given a topological space X and a nonempty index type ι, if t is a directed (under inclusion) family of nonempty, compact, and closed sets in X, then their intersection is nonempty.
|
IsCompact.mem_prod_nhdsSet_of_forall
theorem IsCompact.mem_prod_nhdsSet_of_forall :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace Y] {K : Set Y} {l : Filter X} {s : Set (X × Y)},
IsCompact K → (∀ y ∈ K, s ∈ l ×ˢ nhds y) → s ∈ l ×ˢ nhdsSet K
The theorem states that for a certain set `s` of pairs (X, Y), if `s` belongs to the product of a filter `l` and the neighborhood of `y` for every `y` in a compact set `K`, then `s` also belongs to the product of the filter `l` and the neighborhood of the set `K`. In other words, there exists a set `t` in the filter `l` and an open set `U` that contains `K` such that the Cartesian product of `t` and `U` is a subset of `s`.
More concisely: If a set `s` of pairs (X, Y) belongs to the product of a filter `l` and the neighborhood of every `Y` in a compact set `K`, then there exists a set `t` in the filter `l` and an open set `U` containing `K` such that `s` is a subset of the product of `t` and `U`.
|
isClosedMap_snd_of_compactSpace
theorem isClosedMap_snd_of_compactSpace :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : CompactSpace X],
IsClosedMap Prod.snd
The theorem `isClosedMap_snd_of_compactSpace` states that for any types `X` and `Y` equipped with topological structures, if `X` is also a compact space, then the function `Prod.snd` which projects an ordered pair in `X × Y` to its second component in `Y` is a closed map. In mathematical terms, this means that for any closed set `U` in `X × Y`, its image under `Prod.snd`, i.e., all second components of pairs in `U`, forms a closed set in `Y`. The compactness of `X` ensures that this property holds for all such sets `U`.
More concisely: If `X` is a compact space, then the second projection `Prod.snd` of a product space `X × Y` is a closed map.
|
IsCompact.elim_finite_subfamily_closed
theorem IsCompact.elim_finite_subfamily_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
IsCompact s → ∀ (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
This theorem states that for every collection (`ι → Set X`) of closed sets (`t : ι → Set X`) in a topological space (`TopologicalSpace X`), if the intersection of this collection avoids (i.e., has no common elements with) a certain compact set (`s : Set X`), then there exists a finite subcollection (`u`), such that its intersection also avoids the same compact set. In other words, if a compact set does not intersect with the intersection of all sets in a family of closed sets, then there is a finite subset of this family that also does not intersect with the compact set. This is a property of compact sets in topological spaces and is used in various areas of mathematics including analysis and algebraic topology.
More concisely: If a compact set in a topological space does not intersect the intersection of all closed sets in a collection, then it does not intersect the finite intersection of some subcollection of those sets.
|
IsCompact.elim_directed_cover
theorem IsCompact.elim_directed_cover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v} [hι : Nonempty ι],
IsCompact s →
∀ (U : ι → Set X),
(∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → Directed (fun x x_1 => x ⊆ x_1) U → ∃ i, s ⊆ U i
The theorem states that for every compact set `s` in a topological space `X` and for every index set `ι`, if we have an open directed cover `U` of the set `s` (meaning every element of `U` is an open set, `s` is a subset of the union of all elements of `U`, and `U` is directed with respect to the subset inclusion relation), then there exists an element in `U` that contains the set `s`. In other words, even though the cover may have many elements, we can find a single one that includes the whole compact set `s`.
More concisely: Every compact set in a topological space has an open cover with a finite subcover. (The given theorem is a special case of this statement, assuming the cover is directed.)
|
Inducing.isCompact_preimage'
theorem Inducing.isCompact_preimage' :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Inducing f → ∀ {K : Set Y}, IsCompact K → K ⊆ Set.range f → IsCompact (f ⁻¹' K)
The theorem `Inducing.isCompact_preimage'` asserts that for any topological spaces `X` and `Y`, and any function `f` from `X` to `Y` that induces a topology on `Y`, if `K` is a compact set in `Y` and `K` is a subset of the range of `f`, then the preimage of `K` under `f` (i.e. the set of all elements in `X` that map to elements in `K` under `f`) is a compact set in `X`. In mathematical terms, this means that if `f` is a function that preserves the topological structure, and `K` is a compact set, then the 'backward image' of `K` under `f` is also compact.
More concisely: If `f` is a continuous function from a compact space `X` to a Hausdorff space `Y` such that the image of `X` under `f` is a subset of a compact set `K` in `Y`, then the preimage of `K` under `f` is compact in `X`.
|
isCompact_univ_iff
theorem isCompact_univ_iff : ∀ {X : Type u} [inst : TopologicalSpace X], IsCompact Set.univ ↔ CompactSpace X
This theorem states that for any type 'X' equipped with a topological structure, the universal set of 'X' is compact if and only if 'X' itself is a compact space. In terms of mathematics, a space 'X' is compact if for any collection of open covers, there is a finite subcover. Thus, the theorem is saying that this property for the entire space 'X' is equivalent to the same property for the universal set, which includes all elements of 'X'.
More concisely: A topological space 'X' and its universe are compact if and only if each other is.
|
LocallyFinite.finite_of_compact
theorem LocallyFinite.finite_of_compact :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] {f : ι → Set X},
LocallyFinite f → (∀ (i : ι), (f i).Nonempty) → Set.univ.Finite
The theorem `LocallyFinite.finite_of_compact` states that if `X` is a compact space (i.e., a type `X` with a topological structure that satisfies the compactness property), then any locally finite family `f` of non-empty sets in `X` can only have finitely many elements. Here, a family of sets is considered locally finite if for every point in `X`, there exists a neighborhood of that point which intersects only finitely many sets in the family. The theorem is formulated in terms of `Set.Finite`, stating that the universal set of this family of sets, `Set.univ`, is finite.
More concisely: A compact space's topology restricts any locally finite, non-empty set family to having finitely many elements.
|
IsCompact.ultrafilter_le_nhds
theorem IsCompact.ultrafilter_le_nhds :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s → ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
The theorem `IsCompact.ultrafilter_le_nhds` states that for any type `X` with a topological space structure, and any set `s` of `X`, if `s` is compact then for every ultrafilter `f`, if `f` is contained in the principal filter of `s`, then there exists an `x` in `s` such that `f` is contained in the neighborhood filter at `x`. In other words, for compact sets, any ultrafilter that is a superset of the set can be "translated" to be a subset of the neighborhood filter of some point in the set.
More concisely: For any compact subset `s` of a topological space `X` and any ultrafilter `f` containing `s`, there exists an element `x` in `s` such that `f` is contained in the neighborhood filter of `x`.
|
isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis
theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] (b : ι → Set X),
TopologicalSpace.IsTopologicalBasis (Set.range b) →
(∀ (i : ι), IsCompact (b i)) → ∀ (U : Set X), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
This theorem states that for any topological space `X` and an index set `ι`, given a basis `b` of `X` where each element of the basis is a compact set, any open and compact set `U` in `X` is equivalent to a finite union of elements from the basis. More formally, for any compact open set `U`, there exists a finite subset `s` of `ι` such that `U` is equal to the union over `s` of the corresponding basis elements. This theorem essentially characterizes compact open sets in terms of the topological basis composed of compact sets.
More concisely: Every compact open set in a topological space with a basis of compact sets is equal to a finite union of basis elements.
|
ClosedEmbedding.tendsto_cocompact
theorem ClosedEmbedding.tendsto_cocompact :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
ClosedEmbedding f → Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
This theorem states that for any closed embedding `f` between two topological spaces `X` and `Y`, the function `f` has the property of "tending to the cocompact filter". More specifically, for every neighborhood of the cocompact filter in `Y`, the preimage under `f` of this neighborhood is a neighborhood of the cocompact filter in `X`. This property is a characteristic of proper maps, and in particular, it underscores the notion that the preimage of a compact set via a closed embedding is always compact.
More concisely: For any closed embedding between topological spaces, the preimage of a neighborhood of the cocompact filter is a neighborhood of the cocompact filter.
|
Filter.comap_cocompact_le
theorem Filter.comap_cocompact_le :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → Filter.comap f (Filter.cocompact Y) ≤ Filter.cocompact X
This theorem states that for any two types `X` and `Y` with associated topological spaces, and any continuous function `f` from `X` to `Y`, the comap (the inverse image filter) of the cocompact filter on `Y` under the function `f` is less than or equal to the cocompact filter on `X`. This is an equivalent formulation of the property that the continuous image of compact sets are compact. Here, `cocompact` is a filter generated by the complements of compact sets in a given topological space.
More concisely: For any continuous function between topological spaces and the complement of a compact set in the domain, the inverse image filter is contained in the cocompact filter on the codomain.
|
isCompact_univ
theorem isCompact_univ : ∀ {X : Type u} [inst : TopologicalSpace X] [h : CompactSpace X], IsCompact Set.univ
This theorem states that for any type `X` equipped with a topology (denoted by `TopologicalSpace X`) and with the property that it is a compact space (`CompactSpace X`), the universal set of `X` (i.e., the set containing all elements of `X`, denoted by `Set.univ`) is compact. Here, a set is compact if for every nontrivial filter `f` that contains the set, there exists an element `a` in the set such that every set of `f` meets every neighborhood of `a`.
More concisely: In Lean 4, if `X` is a compact topological space, then the universal set of `X` is compact. Equivalently, every cover of `Set.univ` by open sets in `X` has a finite subcover.
|
LocallyFinite.finite_nonempty_inter_compact
theorem LocallyFinite.finite_nonempty_inter_compact :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set X} {f : ι → Set X},
LocallyFinite f → IsCompact s → {i | (f i ∩ s).Nonempty}.Finite
The theorem `LocallyFinite.finite_nonempty_inter_compact` states that given a topological space `X`, if `s` is a compact set in `X` and `f` is a locally finite family of sets mapped from any type `ι` to `Set X`, then the intersection of `f i` and `s` is nonempty only for a finitely many indices `i`. In other words, only a finite number of sets in the family `f` have nonempty intersection with the compact set `s`.
More concisely: Given a compact set `s` in a topological space `X` and a locally finite family `f` of subsets of `X`, the number of sets in `f` intersecting `s` is finite.
|
isCompact_iUnion
theorem isCompact_iUnion :
∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort u_2} {f : ι → Set X} [inst_1 : Finite ι],
(∀ (i : ι), IsCompact (f i)) → IsCompact (⋃ i, f i)
The theorem `isCompact_iUnion` states that for any type `X` with a topological structure and a finite index set `ι`, if each set `f(i)` for `i` in `ι` is compact, then the union of all these sets `f(i)` is also compact. In more mathematical terms, if `f : ι → Set X` is a family of compact subsets indexed by a finite index set `ι`, then the union ⋃_{i in ι} f(i) is also a compact subset of `X`.
More concisely: If `X` is a topological space and `f : ι → Compact X` is a family of compact subsets indexed by a finite set `ι`, then `⋃_{i in ι} f(i)` is a compact subset of `X`.
|
IsCompact.eventually_forall_of_forall_eventually
theorem IsCompact.eventually_forall_of_forall_eventually :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ : X} {K : Set Y},
IsCompact K →
∀ {P : X → Y → Prop},
(∀ y ∈ K, ∀ᶠ (z : X × Y) in nhds (x₀, y), P z.1 z.2) → ∀ᶠ (x : X) in nhds x₀, ∀ y ∈ K, P x y
This theorem states that if we have a compact set `K`, and for every point `y` in `K`, a property `P` holds for a pair `(x, y)` close enough to `(x₀, y₀)`, then it is guaranteed that there exists a region close to `x₀`, such that for any `x` in this region, the property `P` holds for all `y` in `K`. In other words, if `P x y` is eventually true as `(x, y)` approaches `(x₀, y₀)` for all `y` in `K`, then `P x y` is eventually true for all `y` in `K` as `x` approaches `x₀`. Here, 'eventually true' means that there is a neighborhood of the point in question where the property holds true.
This theorem links local behavior (what happens close to each `(x₀, y₀)`) with global behavior (what happens close to `x₀` for all `y` in `K`) in the context of topological spaces, and is a fundamental result in topology with applications in various branches of mathematics. The key condition is that the set `K` is compact, a central notion in topology that roughly means that `K` is 'small' or 'well-contained'.
More concisely: If a property holds for all `(x, y)` close enough to `(x₀, y₀)` for every `y` in a compact set `K`, then there exists a neighborhood of `x₀` where the property holds for all `y` in `K`.
|
IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed
theorem IsCompact.nonempty_iInter_of_sequence_nonempty_compact_closed :
∀ {X : Type u} [inst : TopologicalSpace X] (t : ℕ → Set X),
(∀ (i : ℕ), t (i + 1) ⊆ t i) →
(∀ (i : ℕ), (t i).Nonempty) → IsCompact (t 0) → (∀ (i : ℕ), IsClosed (t i)) → (⋂ i, t i).Nonempty
This theorem is known as Cantor's intersection theorem for sequences indexed by `ℕ` (the set of natural numbers). It states that given a topological space `X` and a sequence `t` of subsets of `X` indexed by natural numbers, if the sequence `t` is decreasing (i.e., for every natural number `i`, `t (i + 1)` is a subset of `t i`), all sets `t i` are nonempty, the first set `t 0` is compact, and all sets `t i` are closed, then the intersection of all sets `t i` (denoted by `⋂ i, t i`) is nonempty. In other words, the intersection of a decreasing sequence of nonempty compact closed sets is nonempty.
More concisely: Given a decreasing sequence of nonempty compact closed sets in a topological space, their intersection is nonempty.
|
isCompact_iff_finite_subfamily_closed
theorem isCompact_iff_finite_subfamily_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s ↔
∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
A set `s` in a topological space `X` is compact if and only if for every family of closed sets (`t` indexed by an index set `ι`), such that the intersection of all `t i` (for all `i` in `ι`) is disjoint from `s`, there exists a finite subfamily `u` such that the intersection of all `t i` (for all `i` in `u`) is still disjoint from `s`. In other words, if `s` avoids the intersection of an arbitrary family of closed sets, then `s` can also avoid the intersection of a finite subfamily of those sets.
More concisely: A set is compact in a topological space if and only if it avoids the intersections of an arbitrary family of closed sets if and only if it avoids the intersections of a finite subfamily of those sets.
|
Filter.mem_cocompact
theorem Filter.mem_cocompact :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s := by
sorry
The theorem `Filter.mem_cocompact` states that for any type `X` equipped with a topological space structure and any set `s` of type `X`, the set `s` is in the filter `Filter.cocompact X` if and only if there exists a set `t` such that `t` is compact and the complement of `t` is a subset of `s`. In other words, a set is in the filter generated by complements to compact sets if it contains the complement of some compact set.
More concisely: A set is in the filter of cocompact subsets of a topological space if and only if it contains the complement of some compact subset.
|
isCompact_iff_finite_subcover
theorem isCompact_iff_finite_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
A set `s` of some type `X` in a topological space is said to be compact if and only if for every open cover of `s`, there exists a finite subcover. Here, an open cover of `s` is a collection of open sets such that `s` is a subset of the union of these open sets. A finite subcover is a finite subcollection of these open sets that still covers `s`. This theorem states the equivalence between this definition of compactness and the one where 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`.
More concisely: A set is compact in a topological space if and only if every open cover has a finite subcover, which is equivalent to every nontrivial filter containing the set having an element meeting every neighborhood of some point in the set.
|
IsCompact.finite_of_discrete
theorem IsCompact.finite_of_discrete :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [inst_1 : DiscreteTopology X], IsCompact s → s.Finite := by
sorry
The theorem `IsCompact.finite_of_discrete` states that for any type `X` and a set `s` of that type, given that `X` has a discrete topology, if the set `s` is compact then it must also be finite. In other words, in a discrete topological space, all compact sets are finite. The terms compact and finite are defined with respect to some specific topological and set properties: 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 intersects every neighborhood of the element. A set is finite if it is equivalent to a set of natural numbers up to some `n`.
More concisely: In a discrete topological space, every compact set is finite.
|
isClosedMap_fst_of_compactSpace
theorem isClosedMap_fst_of_compactSpace :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : CompactSpace Y],
IsClosedMap Prod.fst
The theorem `isClosedMap_fst_of_compactSpace` states that if `Y` is a compact topological space, then the first projection function `Prod.fst : X × Y → X`, which takes a pair and returns its first component, is a closed map. In other words, for any closed set `U` in the product space `X × Y`, its image under `Prod.fst` is a closed set in `X`. This holds for all types `X` and `Y`, given that `X` and `Y` have topological space structures and `Y` is compact.
More concisely: If `X` and `Y` are topological spaces with `Y` compact, then the first projection map `Prod.fst : X × Y → X` is aclosed map, meaning the image of any closed subset of `X × Y` under `Prod.fst` is a closed subset of `X`.
|
IsCompact.tendsto_nhds_of_unique_mapClusterPt
theorem IsCompact.tendsto_nhds_of_unique_mapClusterPt :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] {s : Set X} {l : Filter Y} {y : X} {f : Y → X},
IsCompact s → (∀ᶠ (x : Y) in l, f x ∈ s) → (∀ x ∈ s, MapClusterPt x l f → x = y) → Filter.Tendsto f l (nhds y)
In the context of a topological space `X` and any types `X` and `Y`, this theorem states that if we have a function `f` mapping from `Y` to `X`, a filter `l` on `Y`, and a compact set `s` in `X`, such that the values of `f` belong to `s` eventually along `l`, and a unique point `y` in `s` is a cluster point for `f` along `l`, then `f` tends to the neighborhood filter of `y` along `l`.
In simpler terms, if the outputs of a function eventually land in a compact set, and there's a unique 'limit point' in that set where outputs accumulate, then that function converges to that limit point in the limit.
More concisely: If a function from a filter on a space to a compact set has a unique cluster point in the image and values belong to the neighborhood filter of that point along the filter, then the function converges to that point along the filter.
|
IsCompact.prod
theorem IsCompact.prod :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
IsCompact s → IsCompact t → IsCompact (s ×ˢ t)
The theorem `IsCompact.prod` states that for any two types `X` and `Y` each equipped with a topological space structure, and for any two sets `s` of type `X` and `t` of type `Y`, if `s` is compact and `t` is compact, then the cartesian product of `s` and `t`, denoted by `s ×ˢ t`, is also compact. In other words, the compactness property is preserved under the formation of cartesian products in topological spaces.
More concisely: If `X` and `Y` are topological spaces with compact sets `s` and `t`, then the cartesian product `s ×ˢ t` is also compact.
|
IsCompact.elim_finite_subcover_image
theorem IsCompact.elim_finite_subcover_image :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X},
IsCompact s → (∀ i ∈ b, IsOpen (c i)) → s ⊆ ⋃ i ∈ b, c i → ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
The theorem `IsCompact.elim_finite_subcover_image` states the following:
For every type `X` and index type `ι`, given a topological space over `X`, a set `s` of type `X`, another set `b` of type `ι`, and a function `c` mapping from `ι` to the set of type `X`, if `s` is compact and for all `i` in `b`, the image of `i` under `c` is an open set, and if `s` is a subset of the union over `i` in `b` of the images of `i` under `c`, then there exists a finite subset `b'` of `b` such that `s` is a subset of the union over `i` in `b'` of the images of `i` under `c`.
In simpler terms, this is a formal statement of the property of compact sets that every open cover has a finite subcover.
More concisely: If `X` is a compact topological space, and `{U_i | i ∈ I}` is an open cover of `X`, then there exists a finite subcover `{U_i_1, ..., U_i_n} ⊆ {U_i | i ∈ I}`.
|
isCompact_of_finite_subfamily_closed
theorem isCompact_of_finite_subfamily_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
(∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅) →
IsCompact s
The theorem `isCompact_of_finite_subfamily_closed` states that a set `s` in a topological space `X` is compact if for every indexed family of closed sets `t` (indexed by `ι`) such that the intersection of all `t i` does not intersect `s`, there exists a finite subfamily `u` of `ι` whose intersection also does not intersect `s`. In other words, if `s` is always avoidable by intersecting enough closed sets from any family, then `s` is a compact set in the topological space `X`.
More concisely: A set in a topological space is compact if and only if for every family of closed sets whose intersection does not intersect the set, there exists a finite subfamily whose intersection also does not intersect the set.
|
Filter.cocompact_eq_bot
theorem Filter.cocompact_eq_bot :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X], Filter.cocompact X = ⊥
This theorem states that for any type `X` equipped with a topological space structure and also being a compact space (i.e., any subset of `X` can be covered by a finite number of open sets in `X`), the filter generated by the complements of compact sets in `X`, denoted as `Filter.cocompact X`, is equal to the bottom filter (`⊥`). The bottom filter is the filter containing all subsets of `X`.
More concisely: For any compact topological space X, the filter of all subsets of X whose complements are compact is equal to the bottom filter.
|
Mathlib.Topology.Compactness.Compact._auxLemma.3
theorem Mathlib.Topology.Compactness.Compact._auxLemma.3 :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s = ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
This theorem states that a set `s` in a topological space `X` is compact if and only if, for any ultrafilter `f` that contains `s` (in other words, for any ultrafilter `f` for which `s` is a subset of every set in `f`), there exists an element `x` in `s` such that `f` is less than or equal to the neighborhood filter at `x`. Here, an ultrafilter is a special kind of filter, and a neighborhood filter at `x` is the collection of all neighborhoods or open sets containing `x`. Intuitively, this is saying that compactness of a set can be characterized by the property that every ultrafilter on the set can be "narrowed down" to a particular point's neighborhood.
More concisely: A set in a topological space is compact if and only if, for every ultrafilter containing the set, there exists an element with the ultrafilter being less than or equal to its neighborhood filter.
|
isCompact_range
theorem isCompact_range :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : CompactSpace X]
{f : X → Y}, Continuous f → IsCompact (Set.range f)
This theorem asserts that for every two types `X` and `Y` where `X` is a compact space and `Y` is a topological space, if a function `f` maps from `X` to `Y` and is continuous, then the range of `f` (i.e., the set of all the images of elements in `X` under `f`) is compact. In other words, for any nontrivial filter `f` that contains the range of `f`, there exists a point in the range such that every set of `f` intersects every neighborhood of that point. This theorem links the concepts of continuity and compactness, showing that the continuous image of a compact space is also compact.
More concisely: A continuous function from a compact space to a topological space maps compact sets to compact sets. (The range of a continuous function from a compact space is a compact subset of the target space.)
|
IsCompact.compl_mem_cocompact
theorem IsCompact.compl_mem_cocompact :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → sᶜ ∈ Filter.cocompact X
The theorem `IsCompact.compl_mem_cocompact` asserts that for any topological space `X` and any set `s` in `X`, if `s` is compact, then the complement of `s` is in the cocompact filter of `X`. In other words, it states that the complement of any compact set is a member of the filter generated by the complements of compact sets in the given topological space.
More concisely: If a set in a topological space is compact, then the complement of that set belongs to the filter generated by the complements of compact sets in the space.
|
IsCompact.elim_finite_subcover
theorem IsCompact.elim_finite_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
IsCompact s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
This theorem states that for every open cover of a compact set in a topological space, there exists a finite subcover. More specifically, given any type `X` with a topological structure, a compact set `s` of type `X`, and an indexed family `U` of open sets in `X` such that `s` is a subset of the union of these sets (i.e., `s` is covered by `U`), there exists a finite subset `t` of the index type such that `s` is also a subset of the union of the sets in `U` indexed by `t`. This is a formalization of the standard concept of compactness in topology.
More concisely: Every compact set in a topological space can be covered by a finite number of open sets from the cover.
|
IsCompact.inter_right
theorem IsCompact.inter_right :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsClosed t → IsCompact (s ∩ t)
The theorem `IsCompact.inter_right` states that for any topological space `X` and any two sets `s` and `t` of `X`, if `s` is a compact set and `t` is a closed set, then the intersection of `s` and `t` (denoted by `s ∩ t`) is also a compact set. In mathematical terms, compactness and closure properties are preserved under intersection in a topological space.
More concisely: If `s` is a compact and `t` is a closed set in a topological space, then their intersection `s ∩ t` is a compact set.
|
Subtype.isCompact_iff
theorem Subtype.isCompact_iff :
∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {s : Set { x // p x }},
IsCompact s ↔ IsCompact (Subtype.val '' s)
This theorem states that for any given type `X` with a topological space structure, a predicate `p : X → Prop`, and a set `s` of elements of subtype `{x // p x}`, the set `s` is compact if and only if the image of `s` under the coercion function `Subtype.val` is compact. Here, compactness of a set is defined in terms of filters: 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 intersects every neighborhood of that element. The coercion function `Subtype.val` is used to retrieve the underlying element of a subtype.
More concisely: For any topological space `X` with a subtype `{x // p x}`, the subtype is compact if and only if its image under the coercion function is a compact subset of `X`.
|
IsCompact.mem_nhdsSet_prod_of_forall
theorem IsCompact.mem_nhdsSet_prod_of_forall :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] {K : Set X} {l : Filter Y} {s : Set (X × Y)},
IsCompact K → (∀ x ∈ K, s ∈ nhds x ×ˢ l) → s ∈ nhdsSet K ×ˢ l
The theorem `IsCompact.mem_nhdsSet_prod_of_forall` states that, for any given types `X` and `Y` with `X` having a topological space structure, a set `K` of type `X`, a filter `l` of type `Y`, and a set `s` of pairs `(X,Y)`, if `K` is compact and for every `x` in `K`, `s` belongs to the product of the neighborhood of `x` and `l`, then `s` belongs to the product of the neighborhood set of `K` and `l`. In other words, there exist an open set `U` that contains `K` and an element `t` in `l` such that the product set of `U` and `t` is a subset of `s`.
More concisely: If `K` is a compact subset of a topological space `X`, and for each `x` in `K`, there exists a neighborhood `U` of `x` and an element `t` in a filter `l` on `X` such that `(x, t)` is in the product of `U` and `l`, then the product of the neighborhood set of `K` and `l` contains `s`.
|
noncompactSpace_of_neBot
theorem noncompactSpace_of_neBot :
∀ {X : Type u} [inst : TopologicalSpace X], (Filter.cocompact X).NeBot → NoncompactSpace X
The theorem `noncompactSpace_of_neBot` states that for any topological space `X`, if the filter generated by complements to compact sets in `X` (denoted as `Filter.cocompact X`) is not the trivial filter (i.e., it contains more than just the entire set), then `X` is a noncompact space. In other words, if there exists a sequence in `X` that does not have any convergent subsequence, which implies that the filter generated by complements to compact sets is not trivial, then `X` is not compact.
More concisely: If the filter of cocompact sets in a topological space is nontrivial, then the space is noncompact.
|
IsCompact.disjoint_nhdsSet_left
theorem IsCompact.disjoint_nhdsSet_left :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X},
IsCompact s → (Disjoint (nhdsSet s) l ↔ ∀ x ∈ s, Disjoint (nhds x) l)
This theorem states that for a given compact set 's' in a topological space 'X' and a filter 'l', the neighborhood filter of the set 's' is disjoint with the filter 'l' if and only if the neighborhood filter of each point in the set 's' is disjoint with the filter 'l'. In other words, there is no overlap between the collection of neighborhoods of the set 's' and the filter 'l' if and only if there is no overlap between the collection of neighborhoods of each individual point in 's' and the filter 'l'.
More concisely: For a compact set $S$ in a topological space $X$ and a filter $l$, the neighborhood filter of $S$ is disjoint with $l$ if and only if the neighborhood filter of each point in $S$ is disjoint with $l$.
|
Set.Finite.isCompact_biUnion
theorem Set.Finite.isCompact_biUnion :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set ι} {f : ι → Set X},
s.Finite → (∀ i ∈ s, IsCompact (f i)) → IsCompact (⋃ i ∈ s, f i)
The theorem `Set.Finite.isCompact_biUnion` states that, for an arbitrary type `X` with a topological space structure, a set `s` of an arbitrary type `ι`, and a function `f` from `ι` to a set of `X`, if `s` is finite and each set `f(i)` for `i` in `s` is compact, then the union of all the sets `f(i)` for `i` in `s` is also compact. In other words, the finite union of compact sets is also compact.
More concisely: If `X` is a topological space, `s` is a finite set, and each `f(i)` is a compact subset of `X` for all `i` in `s`, then the union of `{f(i) | i ∈ s}` is a compact subset of `X`.
|
IsCompact.elim_directed_family_closed
theorem IsCompact.elim_directed_family_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v} [hι : Nonempty ι],
IsCompact s →
∀ (t : ι → Set X),
(∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → Directed (fun x x_1 => x ⊇ x_1) t → ∃ i, s ∩ t i = ∅
The theorem `IsCompact.elim_directed_family_closed` states that for any compact set `s` in a topological space `X`, given a directed family of closed sets `t` (where the directed relation is defined by subset inclusion), if the intersection of `s` and the intersection of all sets in the family `t` is empty, then there exists a single set within the family `t` whose intersection with `s` is also empty. In other words, if a compact set avoids the intersection of a directed family of closed sets, then it also avoids at least one member of that family.
More concisely: If a compact set in a topological space intersects empty with the intersection of a directed family of closed sets, then it intersects empty with some set in the family.
|
Filter.mem_cocompact'
theorem Filter.mem_cocompact' :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t := by
sorry
The theorem `Filter.mem_cocompact'` states that for any type `X`, equipped with a topological structure, and for any set `s` of type `X`, the set `s` is a member of the filter `cocompact` of `X` if and only if there exists a set `t` which is compact and the complement of `s` is a subset of `t`. Here, a set `t` is said to be compact if for every non-trivial filter `f` that contains `t`, there exists an element `a` in `t` such that every set of `f` intersects every neighborhood of `a`. The `cocompact` filter of `X` is the filter generated by the complements of all compact sets in `X`.
More concisely: A set `s` in a topological space `X` belongs to the cocompact filter if and only if its complement is a subset of some compact set.
|
IsCompact.compl_mem_sets
theorem IsCompact.compl_mem_sets :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s → ∀ {f : Filter X}, (∀ x ∈ s, sᶜ ∈ nhds x ⊓ f) → sᶜ ∈ f
The theorem `IsCompact.compl_mem_sets` states the following: given a topological space `X` and a set `s` in `X` that is compact, for any filter `f` on `X`, if the complement of `s` belongs to each filter generated by the intersection of the neighborhood filter of `x` and `f` for every `x` in `s`, then the complement of `s` belongs to `f`. In simpler terms, if the complement of a compact set is in every intersected filter of the neighborhoods of points in the set and `f`, then that complement is also in `f`. The concept of compactness is a key idea in topology and has important implications in the convergence and boundedness properties of functions.
More concisely: If a compact subset `s` of a topological space `X` is such that the complement of `s` is contained in every filter generated by the intersections of the neighborhood filters of points in `s` and a filter `f`, then the complement of `s` is contained in `f`.
|
Mathlib.Topology.Compactness.Compact._auxLemma.4
theorem Mathlib.Topology.Compactness.Compact._auxLemma.4 :
∀ {α : Type u} {s : Set α} {f : Filter α}, (f ≤ Filter.principal s) = (s ∈ f)
This theorem states that for any type `α`, any set `s` of type `α`, and any filter `f` of type `α`, the filter `f` is less than or equal to the principal filter of `s` if and only if `s` is a member of filter `f`. Here, the principal filter of `s` is the collection of all supersets of `s`, and a filter `f` being less than or equal to another filter means that every set in `f` is also in the other filter. Thus, this theorem establishes an equivalence between `s` being in filter `f` and `f` including all supersets of `s`.
More concisely: Given any type `α`, set `s` of type `α`, and filter `f` over `α`, `s` is a member of `f` if and only if `f` includes the principal filter of `s`.
|
IsCompact.elim_nhds_subcover
theorem IsCompact.elim_nhds_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s → ∀ (U : X → Set X), (∀ x ∈ s, U x ∈ nhds x) → ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
The theorem `IsCompact.elim_nhds_subcover` states that for any type `X` equipped with a topology and any compact set `s` of type `X`, if for every point `x` in `s`, `U x` is a neighborhood of `x` (i.e., `U x` belongs to the neighborhood filter of `x`), then there exists a subset `t` of `s` such that every point in `s` is in the union of the sets `U x` for `x` in `t`. In other words, the set `s` can be covered by a subcollection of the neighborhoods `U x`, where `x` ranges over the points in the compact set `s`. This theorem captures one of the fundamental properties of compact sets in topology: every open cover has a finite subcover.
More concisely: Given a compact set `s` in a topological space `X` such that for each `x` in `s`, `U x` is a neighborhood of `x`, there exists a finite subcover `t` of `{U x | x ∈ s}` that covers `s`.
|
IsCompact.ultrafilter_le_nhds'
theorem IsCompact.ultrafilter_le_nhds' :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s → ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x
The theorem `IsCompact.ultrafilter_le_nhds'` states that for any topological space `X` and any set `s` in `X`, if `s` is compact, then for any ultrafilter `f` that contains `s`, there exists an element `x` in `s` such that the ultrafilter `f` is less than or equal to the neighborhood filter at `x`. In other words, in a compact set in a topological space, any ultrafilter on that set 'converges' to at least one point in the set, in the sense that every neighborhood of that point intersects with the ultrafilter.
More concisely: In a compact topological space, every ultrafilter containing a subset has an element that lies in the subset and is contained in the ultrafilter's neighborhood filter.
|
LocallyFinite.finite_nonempty_of_compact
theorem LocallyFinite.finite_nonempty_of_compact :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] {f : ι → Set X},
LocallyFinite f → {i | (f i).Nonempty}.Finite
This theorem states that if `X` is a compact space, then any locally finite family of sets of `X` can have only finitely many nonempty elements. In other words, given a compact topological space `X` and a family of sets `f` from `X` which is locally finite, the set of indices `i` for which the corresponding set `f i` is nonempty is finite. This theorem highlights a property of compact spaces, where compactness imposes strong finiteness conditions on the collections of subsets of the space.
More concisely: A compact space's locally finite family of sets has finitely many nonempty members.
|
isCompact_singleton
theorem isCompact_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, IsCompact {x}
The theorem `isCompact_singleton` states that for any type `X` equipped with a topological space structure, every singleton set `{x}` is compact. In other words, for any given filter `f` that is not trivial and contains `{x}`, there exists a point in `{x}` (which is `x` itself) such that every set of `f` meets every neighborhood of `x`.
More concisely: For any topological space `(X, τ)` and point `x ∈ X`, the singleton set `{x} ⊆ X` is compact.
|
IsCompact.image
theorem IsCompact.image :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
IsCompact s → Continuous f → IsCompact (f '' s)
The theorem `IsCompact.image` states that for any two topological spaces `X` and `Y`, a set `s` from `X`, and a function `f` from `X` to `Y`, if the set `s` is compact and the function `f` is continuous, then the image of the set `s` under the function `f` is also compact. In mathematical terms, if \(s\) is a compact set in a topological space \(X\) and \(f: X \to Y\) is a continuous function, then \(f(s)\) is a compact set in the topological space \(Y\).
More concisely: If a compact set in a topological space is mapped by a continuous function to another topological space, the image is also a compact set.
|
IsCompact.diff
theorem IsCompact.diff :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsCompact s → IsOpen t → IsCompact (s \ t)
The theorem `IsCompact.diff` states that in any topological space `X`, if `s` is a compact set and `t` is an open set, then the set difference of `s` and `t`, denoted `(s \ t)`, is also a compact set. In other words, subtracting an open set from a compact set still leaves us with a compact set. This is an important result in topology, which helps to understand the properties and behavior of compact sets in different contexts.
More concisely: In any topological space, the difference of a compact set and an open set is a compact set.
|
Embedding.isCompact_iff
theorem Embedding.isCompact_iff :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
Embedding f → (IsCompact s ↔ IsCompact (f '' s))
The theorem `Embedding.isCompact_iff` states that for any two types `X` and `Y` with respective topological space instances, a set `s` of type `X`, and a function `f` from `X` to `Y`, if `f` is an embedding then the image of the set `s` under the function `f`, denoted `f '' s`, is compact if and only if `s` itself is compact. In other words, an embedding preserves the compactness of sets.
More concisely: An embedding of a compact topological space preserves the compactness of sets: if a function between two topological spaces is an embedding and its domain is a compact set, then the image of that set under the function is also compact.
|
ClosedEmbedding.isCompact_preimage
theorem ClosedEmbedding.isCompact_preimage :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
ClosedEmbedding f → ∀ {K : Set Y}, IsCompact K → IsCompact (f ⁻¹' K)
The theorem `ClosedEmbedding.isCompact_preimage` states that for any two types `X` and `Y` equipped with topological spaces, a function `f` from `X` to `Y`, and a set `K` in `Y` that is compact, if `f` is a closed embedding (which means it is a function that is continuous, injective, and its image is a closed set), then the preimage of `K` under `f` (the set of all elements in `X` that `f` maps into `K`) is also a compact set. In other words, the preimage of a compact set under a closed embedding retains the property of compactness.
More concisely: If `f : X ⟹ Y` is a closed embedding of topological spaces and `K ⊆ Y` is compact, then `f⁻¹(K) ⊆ X` is also compact.
|
IsCompact.le_nhds_of_unique_clusterPt
theorem IsCompact.le_nhds_of_unique_clusterPt :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s → ∀ {l : Filter X} {y : X}, s ∈ l → (∀ x ∈ s, ClusterPt x l → x = y) → l ≤ nhds y
This theorem states that in a topological space `X`, if a compact set `s` is contained in a filter `l` and this filter has a unique cluster point `y` within this set, then the filter is less than or equal to the neighborhood of `y`. In other words, if `l` is a filter on `X` which is associated with a compact set in such a way that there's a specific point `y` in the set where all points in the compact set that are cluster points of the filter coincide with `y`, then the filter `l` is a subset of (or equal to) the set of all neighborhoods of `y`. This theorem is a characteristic property of compact sets in topological spaces.
More concisely: If a compact set in a topological space is contained in a filter with a unique cluster point, then the filter is contained in the neighborhood system of that point.
|
IsCompact.disjoint_nhdsSet_right
theorem IsCompact.disjoint_nhdsSet_right :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X},
IsCompact s → (Disjoint l (nhdsSet s) ↔ ∀ x ∈ s, Disjoint l (nhds x))
This theorem states that for a given topological space `X`, a set `s` in `X`, and a filter `l`, if the set `s` is compact, then `l` is disjoint with the neighborhood filter of the set `s` if and only if `l` is disjoint with the neighborhood filter of each point in the set `s`. In other words, a filter is disjoint with the neighborhood filter of a compact set precisely when it is disjoint with the neighborhood filters of all points in the set.
More concisely: A filter is disjoint with the neighborhood filter of a compact set if and only if it is disjoint with the neighborhood filters of all points in the set.
|
Filter.mem_coclosedCompact
theorem Filter.mem_coclosedCompact :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
s ∈ Filter.coclosedCompact X ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ s
The theorem `Filter.mem_coclosedCompact` states that for any type `X` equipped with a topology and any set `s` of type `X`, `s` is in the filter generated by complements of closed compact sets if and only if there exists a set `t` such that `t` is closed, `t` is compact and the complement of `t` is a subset of `s`. In other words, the set `s` belongs to the filter of complements of closed compact sets precisely when we can find a closed and compact set whose complement is contained within `s`.
More concisely: A set is in the filter of complements of closed compact sets if and only if it is the complement of some closed and compact set.
|
IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
theorem IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed :
∀ {X : Type u} [inst : TopologicalSpace X] (t : ℕ → Set X),
(∀ (i : ℕ), t (i + 1) ⊆ t i) →
(∀ (i : ℕ), (t i).Nonempty) → IsCompact (t 0) → (∀ (i : ℕ), IsClosed (t i)) → (⋂ i, t i).Nonempty
The theorem `IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed` is known as Cantor's intersection theorem for sequences indexed by ℕ (the set of natural numbers). It states that if we have a topological space `X` and a sequence of sets `t` indexed by the natural numbers (i.e., `t : ℕ → Set X`), where each set in the sequence is a subset of the previous one (i.e., `∀ (i : ℕ), t (i + 1) ⊆ t i`), and every set in the sequence is nonempty and closed, with the first set being compact (i.e., `∀ (i : ℕ), Set.Nonempty (t i)`, `IsCompact (t 0)`, and `∀ (i : ℕ), IsClosed (t i)`), then the intersection of all sets in the sequence is also nonempty (i.e., `Set.Nonempty (⋂ i, t i)`). This theorem is a fundamental result in topology, highlighting the peculiar properties of compact sets.
More concisely: If `X` is a topological space, `t : ℕ → Set X` is a decreasing sequence of nonempty, closed, and compact sets in `X` with `t 0` compact, then their intersection is nonempty.
|
Filter.coprod_cocompact
theorem Filter.coprod_cocompact :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
(Filter.cocompact X).coprod (Filter.cocompact Y) = Filter.cocompact (X × Y)
This theorem states that for any two topological spaces `X` and `Y`, the coproduct of their cocompact filters is equal to the cocompact filter on the product space `X × Y`. Here, a cocompact filter is defined as a filter generated by the complements of compact sets in a given topological space. The coproduct operation refers to a way of combining two filters.
More concisely: For any topological spaces X and Y, the cocompact filter on X × Y is equal to the coproduct of the cocompact filters on X and Y.
|
IsCompact.prod_nhdsSet_eq_biSup
theorem IsCompact.prod_nhdsSet_eq_biSup :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace Y] {K : Set Y},
IsCompact K → ∀ (l : Filter X), l ×ˢ nhdsSet K = ⨆ y ∈ K, l ×ˢ nhds y
This theorem states that for all given types `X` and `Y` with `Y` a topological space and `K` a compact set in `Y`, and for any filter `l` on `X`, the product of the filter `l` and the filter of neighborhoods of the set `K` is equivalent to the supremum over all elements `y` in `K` of the product of the filter `l` and the filter of neighborhoods of `y`. In other words, the set of neighborhoods of a compact set is equivalent to the union of the set of neighborhoods of each of its points when considered in conjunction with a particular filter on another space.
More concisely: For any compact set K in a topological space Y and filter l on X, the product filter of l and the filter of neighborhoods of K is equal to the supremum of the product of l and the filter of neighborhoods of each point in K.
|
isCompact_iff_ultrafilter_le_nhds
theorem isCompact_iff_ultrafilter_le_nhds :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
This theorem states that for any topological space `X` and any set `s` of `X`, the set `s` is compact if and only if for any ultrafilter `f` on `X`, if `f` is contained in the principal filter of `s`, then there exists an element `x` in `s` such that `f` is also contained in the neighborhood filter at `x`.
In mathematical terms, this implies that in a compact set, every ultrafilter (a maximally fine way of describing "large" subsets of `X`) that contains the set must "converge" to some point within the set. That is, every "large" subset of `s` (as identified by the ultrafilter) must have nonempty intersection with every neighborhood of that point. This is an alternative characterization of compactness in terms of filter theory.
More concisely: A set in a topological space is compact if and only if every ultrafilter containing the set intersects the neighborhood filter of some point in the set.
|
Set.Finite.isCompact
theorem Set.Finite.isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s.Finite → IsCompact s := by
sorry
This theorem states that for any type `X` that has a topological space structure, any finite set `s` of elements of type `X` is compact. Here, a set `s` is said to be compact if for every nontrivial filter `f` that contains `s`, there exists an element `x` in `s` such that every set in `f` meets every neighborhood of `x`. A set is said to be finite if there exists a natural number `n` and an equivalence between the set and `Fin n`.
More concisely: For any topological space `X`, every finite subset `s` of `X` is compact in the sense that for every nontrivial filter `f` containing `s`, there exists an element `x` in `s` such that every set in `f` intersects every neighborhood of `x`.
|