Mathlib.Topology.Order.UpperLowerSetTopology._auxLemma.1
theorem Mathlib.Topology.Order.UpperLowerSetTopology._auxLemma.1 :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpperSet α] {s : Set α},
IsOpen s = IsUpperSet s
This theorem, `Mathlib.Topology.Order.UpperLowerSetTopology._auxLemma.1`, states that for any type `α`, under the conditions that `α` has a preorder structure, a topological space structure, and a topology that respects this preorder as an upper set, for any set `s` of type `α`, `s` is open in the topological space if and only if `s` is an upper set in the preorder. In other words, a set is open in the given topological space if it has the property that any element greater than one of its members is also a member. The theorem creates an equivalence between the topological concept of 'openness' and the order-theoretic concept of 'being an upper set'.
More concisely: A set in a preordered topological space is open if and only if it is an upper set with respect to the preorder.
|
Topology.IsLowerSet.closure_singleton
theorem Topology.IsLowerSet.closure_singleton :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLowerSet α] {a : α},
closure {a} = Set.Ici a
The theorem `Topology.IsLowerSet.closure_singleton` states that for any type `α` with a preorder and a lower set topology, the closure of a singleton set `{a}` is the right-closed, left-infinite interval `(-∞,a]`. In other words, the smallest closed set that contains only the element `a` is the set of all elements `x` such that `a ≤ x` in the context of a lower set topology.
More concisely: In a lower set topology of a preordered type `α`, the closure of the singleton set `{a}` is the right-closed, left-infinite interval `(-∞, a]`.
|
Topology.IsUpperSet.topology_eq
theorem Topology.IsUpperSet.topology_eq :
∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpperSet α],
inst_1 = Topology.upperSet α
This theorem states that for any type `α` with a preorder and a topological space structure, if the topological space structure is such that its open sets are exactly the upper sets, then this topology is equal to the "upper set topology" on `α`. The upper set topology is defined to be the topology whose open sets are precisely the upper sets in the preorder.
More concisely: For any type `α` with a preorder, if its topological space structure makes open sets equal to upper sets in the preorder, then this topology is the upper set topology.
|
Topology.IsUpperSet.closure_singleton
theorem Topology.IsUpperSet.closure_singleton :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpperSet α] {a : α},
closure {a} = Set.Iic a
This theorem states that in any preordered set equipped with the upper set topology, the closure of a singleton set containing a single element `a` is equivalent to the set of all elements that are less than or equal to `a`. In other words, the closure of `{a}` in this particular topological space is the right-closed, left-infinite interval `(-∞, a]`. Hence, every point less than or equal to `a` is in the closure of `{a}`, and there are no points greater than `a` in the closure.
More concisely: In a preordered set with upper set topology, the closure of a singleton set is equal to the set of elements less than or equal to the element in the set.
|
Topology.IsLowerSet.topology_eq
theorem Topology.IsLowerSet.topology_eq :
∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLowerSet α],
inst_1 = Topology.lowerSet α
This theorem states that for any type `α` with a preorder structure, and equipped with a topological space and lower set topology, the topological space is equivalent to the lower set topology. In other words, if a topology on a preordered type is defined in such a way that its open sets are lower sets, then this topology is exactly the same as the lower set topology on that type.
More concisely: For any preordered type `α` with a topology making open sets equivalent to lower sets, the topology is identical to the lower set topology.
|