isClopen_inter_of_disjoint_cover_clopen
theorem isClopen_inter_of_disjoint_cover_clopen :
∀ {X : Type u} [inst : TopologicalSpace X] {s a b : Set X},
IsClopen s → s ⊆ a ∪ b → IsOpen a → IsOpen b → Disjoint a b → IsClopen (s ∩ a)
This theorem states that within a particular topological space X, if we have a set 's' that is clopen (i.e., both closed and open), and 's' is a subset of the union of two sets 'a' and 'b', which are both open and disjoint (i.e., their intersection is the empty set), then the intersection of 's' and 'a' will also be a clopen set.
More concisely: If in a topological space X, 's' is a clopen subset of the disjoint open sets 'a' and 'b', then the intersection of 's' and 'a' is a clopen set.
|
IsClopen.isOpen
theorem IsClopen.isOpen : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → IsOpen s
This theorem states that for any type `X` and a topological space `inst` over `X`, if a set `s` of type `X` is both closed and open (i.e., it is clopen), then it is open in the context of the ambient topological space. In mathematical terms, if a set is clopen in a given topological space, it implies that the set is open in that space.
More concisely: If a set is clopen in a topological space, then it is open in that space.
|
IsClopen.compl
theorem IsClopen.compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → IsClopen sᶜ
The theorem `IsClopen.compl` states that for any type `X` equipped with a topological space structure and any set `s` of type `X`, if `s` is a clopen set (i.e., both closed and open), then the complement of `s` (denoted as `sᶜ`) is also a clopen set. In other words, the property of being clopen is preserved under the operation of taking complements in the context of topological spaces.
More concisely: If a set is clopen in a topological space, then its complement is also clopen.
|
IsClopen.frontier_eq
theorem IsClopen.frontier_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → frontier s = ∅ := by
sorry
This theorem, referred to by the alias `IsClopen.frontier_eq`, states that for any given type `X` that has a topology (as defined by the presence of a `TopologicalSpace X` instance), if a set `s` of type `X` is clopen (meaning it is both closed and open), then the frontier of that set is empty. In other words, if a set is simultaneously closed and open in a given topological space, it has no points that lie between its closure and interior. In mathematical terms, this is written as if $s$ is clopen, then the frontier of $s$ equals the empty set.
More concisely: If a set in a topological space is both closed and open, then its frontier is empty.
|