TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage
theorem TopologicalSpace.Compacts.coe_equiv_apply_eq_preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β)
(K : TopologicalSpace.Compacts α), ↑((TopologicalSpace.Compacts.equiv f) K) = ⇑f.symm ⁻¹' ↑K
This theorem states that, given any topological spaces `α` and `β`, and a homeomorphism `f` from `α` to `β`, for any compact set `K` in `α`, the image of `K` under the induced equivalence of compact sets by `f` is equivalent to the preimage of `K` under the inverse of `f`. In simpler words, this theorem implies that applying a homeomorphism to a compact set and then taking the preimage under the inverse of the homeomorphism will give you back the original compact set.
More concisely: Given any compact sets $K$ in topological spaces $\alpha$ and $\beta$, and a homeomorphism $f:\alpha \to \beta$ between them, the image of $K$ under $f$ is homeomorphic to the preimage of $K$ under $f^{-1}$.
|
TopologicalSpace.PositiveCompacts.isCompact
theorem TopologicalSpace.PositiveCompacts.isCompact :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α), IsCompact ↑s
This theorem states that for any topological space `α` and any `s` belonging to the set of positive compacts of `α`, `s` is compact. In mathematical terms, this means for every nontrivial filter `f` that contains `s`, there is an element `a` in `s` such that every set in `f` intersects every neighborhood of `a`.
More concisely: Every positive compact subset of a topological space is compact.
|
TopologicalSpace.Compacts.isCompact
theorem TopologicalSpace.Compacts.isCompact :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.Compacts α), IsCompact ↑s
The theorem `TopologicalSpace.Compacts.isCompact` states that for any type `α` equipped with a topology (i.e., `α` is a topological space) and any compact subset `s` of this topological space, `s` has the property of being compact. Here, a set is defined to be compact if, for every nontrivial filter `f` that contains the set, there exists a point `x` in the set such that all sets in the filter `f` intersect every neighborhood of `x`.
More concisely: A compact subset of a topological space is a set such that for every nontrivial filter containing it, there exists an element in the set intersecting every neighborhood of that element.
|
TopologicalSpace.CompactOpens.isOpen
theorem TopologicalSpace.CompactOpens.isOpen :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.CompactOpens α), IsOpen ↑s
The theorem `TopologicalSpace.CompactOpens.isOpen` states that for any type `α` with a topological space structure, if `s` is a set in the `CompactOpens` of `α`, then `s` is an open set in the ambient topological space on `α`. Here, the `CompactOpens` of a topological space refers to the collection of open sets that are compact.
More concisely: A compact open set in a topological space is an open set.
|
TopologicalSpace.PositiveCompacts.interior_nonempty
theorem TopologicalSpace.PositiveCompacts.interior_nonempty :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α), (interior ↑s).Nonempty := by
sorry
This theorem, named `TopologicalSpace.PositiveCompacts.interior_nonempty`, asserts that for any topological space `α` and any element `s` of the set `TopologicalSpace.PositiveCompacts α`, the interior of `s` is not empty. Here, `TopologicalSpace.PositiveCompacts α` refers to the set of compact subsets of the topological space `α` that have positive measure. In other words, for any compact subset `s` with positive measure in a given topological space, its interior (the largest open subset of `s`) always contains at least one point.
More concisely: In a topological space, every compact subset of positive measure has a non-empty interior.
|
TopologicalSpace.Compacts.coe_bot
theorem TopologicalSpace.Compacts.coe_bot : ∀ {α : Type u_1} [inst : TopologicalSpace α], ↑⊥ = ∅
This theorem states that for any type `α` equipped with a topological space structure, the compact subspace represented by the bottom element (denoted by `⊥`) is equal to the empty set. In other words, in the context of topological spaces, the compact subset represented by the least information (i.e., `⊥`) corresponds to having no elements at all (i.e., the empty set).
More concisely: For any topological space `α`, the compact subspace containing the bottom element `⊥` is the empty set.
|
TopologicalSpace.PositiveCompacts.ext
theorem TopologicalSpace.PositiveCompacts.ext :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.PositiveCompacts α}, ↑s = ↑t → s = t := by
sorry
This theorem states that for any topological space `α`, and any two 'positive compacts' `s` and `t` in this space, if their underlying sets (obtained by applying the coercion function `↑`) are equal, then `s` and `t` themselves must be equal.
In other words, two 'positive compacts' in a given topological space are identical if and only if their underlying sets are identical. 'Positive compacts' are a type of subset of a topological space that are both compact and non-empty.
More concisely: For any topological space `α`, two positive compacts `s` and `t` are equal if and only if their underlying sets are equal.
|
TopologicalSpace.Compacts.ext
theorem TopologicalSpace.Compacts.ext :
∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.Compacts α}, ↑s = ↑t → s = t
This theorem states that for any type `α` equipped with a topological space structure, if we have two compact subspaces `s` and `t` of this topological space, and if the underlying sets of `s` and `t` are equal, then `s` and `t` must be the same compact subspace. In other words, in a given topology, compact subspaces are uniquely determined by their underlying sets.
More concisely: In a topological space, two compact subsets with equal underlying sets are equal as subspaces.
|
TopologicalSpace.CompactOpens.isCompact
theorem TopologicalSpace.CompactOpens.isCompact :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.CompactOpens α), IsCompact ↑s
The theorem `TopologicalSpace.CompactOpens.isCompact` states that for any type `α` that has a topological space structure and for any set `s` of compact open subsets of `α`, the set `s` is compact. In other words, for every nontrivial filter `f` that contains `s`, there exists an element `x` in `s` such that every set of `f` meets every neighborhood of `x`. This theorem is a property of compact open subsets in topological spaces.
More concisely: A set of compact open subsets of a topological space is compact.
|
TopologicalSpace.NonemptyCompacts.nonempty
theorem TopologicalSpace.NonemptyCompacts.nonempty :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α), (↑s).Nonempty
The theorem `TopologicalSpace.NonemptyCompacts.nonempty` states that for any type `α` which has a topology (i.e., is an instance of a `TopologicalSpace`), and for any nonempty compact subset `s` of the topological space `α` (`TopologicalSpace.NonemptyCompacts α`), the set `s` is not empty (`Set.Nonempty ↑s`). In simple terms, the theorem guarantees that a nonempty compact subset in any topological space is indeed nonempty.
More concisely: In any topological space, every nonempty compact subset is nonempty.
|
TopologicalSpace.NonemptyCompacts.isCompact
theorem TopologicalSpace.NonemptyCompacts.isCompact :
∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.NonemptyCompacts α), IsCompact ↑s
This theorem states that for any type `α` endowed with a topological space structure, if `s` is any non-empty compact subset of `α`, then `s` itself is compact. In mathematical terms, given a topological space `α`, for any non-empty compact subset `s` of `α`, it holds that 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`. This essentially says that the compactness property is preserved in non-empty compact subsets within a topological space.
More concisely: In a topological space, any non-empty compact subset is compact.
|