TopologicalSpace.Clopens.isClopen
theorem TopologicalSpace.Clopens.isClopen :
∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Clopens α), IsClopen ↑s
This theorem states that for any topological space `α` and any clopen set `s` in this space, `s` is both closed and open. In more detail, given a topological space, which is a set with a family of subsets satisfying certain properties, there exists a concept of 'clopen' sets. These are sets that are both closed (complements of open sets) and open (part of the given family of subsets). The theorem confirms that if a set is defined as 'clopen' in the space, it indeed possesses both of these properties.
More concisely: In any topological space, a clopen set is both closed and open.
|
TopologicalSpace.Opens.isCoatom_iff
theorem TopologicalSpace.Opens.isCoatom_iff :
∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {s : TopologicalSpace.Opens α},
IsCoatom s ↔ ∃ x, s = (TopologicalSpace.Closeds.singleton x).compl
This theorem states that in any `T1Space` (a type of topological space where for any pair of distinct points, each has a neighborhood not containing the other), a coatom of the open sets in that space (`TopologicalSpace.Opens α`) is exactly the complement of a singleton set. A coatom in this context is an open set for which there is no other open set strictly between it and the whole space (excluding the whole space itself). Specifically, an open set is a coatom if and only if there exists a point such that the open set is the complement of the closure of the singleton set containing that point (`TopologicalSpace.Closeds.singleton x`).
More concisely: In a T1 space, an open set is a coatom if and only if it is the complement of the closure of a singleton set.
|
TopologicalSpace.Opens.compl_compl
theorem TopologicalSpace.Opens.compl_compl :
∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Opens α), s.compl.compl = s
This theorem states that for every open set `s` in a given topological space, the complement of the complement of `s` is equal to `s` itself. In other words, if you take an open set `s`, find its complement (which is a closed set), and then find the complement of that closed set (which results in an open set), you will end up with the original open set `s`. This corresponds to the general principle in set theory that the complement of the complement of a set is the set itself, but applied specifically to the context of open and closed sets in a topological space.
More concisely: The complement of the complement of an open set equals the original open set in a topological space.
|
TopologicalSpace.Closeds.isAtom_iff
theorem TopologicalSpace.Closeds.isAtom_iff :
∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {s : TopologicalSpace.Closeds α},
IsAtom s ↔ ∃ x, s = TopologicalSpace.Closeds.singleton x
The theorem `TopologicalSpace.Closeds.isAtom_iff` states that in a T1 space, a closed set is an atom of the topological space if and only if it is a singleton. In other words, a closed set, within the context of a T1 topological space, is an atom if there is no other closed set strictly between it and the empty set and it is not the empty set itself. This is precisely the case when the set consists of a single point, i.e., it is a singleton.
More concisely: In a T1 topological space, a closed set is an atom if and only if it is a singleton.
|
TopologicalSpace.Closeds.compl_compl
theorem TopologicalSpace.Closeds.compl_compl :
∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Closeds α), s.compl.compl = s
This theorem states that, for any topological space `α` and for any closed set `s` in this topological space, taking the complement twice - first as an open set, then as a closed set - will result in the original closed set `s`. In more mathematical terms, for a given closed set `s` in topological space `α`, the operation `TopologicalSpace.Opens.compl (TopologicalSpace.Closeds.compl s)` is essentially a double application of set complement, which is an operation that returns the set of elements not in `s`. Since the complement of a complement of a set is the set itself, this operation always returns the original set `s`.
More concisely: For any closed set `s` in a topological space `α`, `TopologicalSpace.Closeds.compl (TopologicalSpace.Opens.compl s)` equals `s`.
|
TopologicalSpace.Closeds.ext
theorem TopologicalSpace.Closeds.ext :
∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Closeds α}, ↑s = ↑t → s = t
This theorem states that for any type `α` that has the structure of a topological space, if we have two subsets `s` and `t` of the set of all closed subsets in `α` such that the type coercion of `s` equals to the type coercion of `t`, then `s` equals to `t`. In other words, this theorem guarantees the uniqueness of each closed subset in the set of all closed subsets of a given topological space.
More concisely: In a topological space `α`, if two subsets `s` and `t` of its closed subsets have equal type coercions, then they are equal.
|