Topology.IsUpper.isClosed_lowerClosure
theorem Topology.IsUpper.isClosed_lowerClosure :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpper α] {s : Set α},
s.Finite → IsClosed ↑(lowerClosure s)
The theorem states that for any type `α` with a preorder and a topological space structure, and furthermore, when this topological space is equipped with the upper topology, the lower closure of any finite set `s` of type `α` is a closed set in this topology. Here, the lower closure of a set `s` is the set of all elements that are less than or equal to some element in `s`. In mathematical terms, if we have a finite set `s` in a topological space that has an upper topology and a preorder, then the set of all points less than or equal to some point in `s` forms a closed set.
More concisely: In a preordered topological space with an upper topology, the lower closure of any finite set is a closed set.
|
Topology.IsUpper.closure_singleton
theorem Topology.IsUpper.closure_singleton :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpper α] (a : α),
closure {a} = Set.Iic a
The theorem `Topology.IsUpper.closure_singleton` states that for any type `α` which has a preorder structure and an upper topology, the closure of a singleton set `{a}` (where `a` is an element of `α`) is equal to the left-infinite right-closed interval `(-∞, a]`. In other words, the smallest closed set containing only the element `a` consists of all elements less than or equal to `a` in the given preorder. This is valid under the upper topology, which is a type of topological space where the closure operation follows specific rules.
More concisely: For any preordered type `α` with an upper topology, the closure of a singleton set `{a}` equals the set `(-∞, a]`.
|
Topology.IsUpper.continuous_iff_Iic
theorem Topology.IsUpper.continuous_iff_Iic :
∀ {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpper α]
[inst_3 : TopologicalSpace β] {f : β → α}, Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)
The theorem `Topology.IsUpper.continuous_iff_Iic` states that for any types `α` and `β`, given that `α` is a preorder and a topological space with an upper topology, and `β` is a topological space, a function `f` from `β` to `α` is continuous if and only if for every `a` in `α`, the preimage of the interval `Set.Iic a` under the function `f` is a closed set. Here, `Set.Iic a` denotes the left-infinite right-closed interval of all elements that are less than or equal to `a`.
More concisely: A function between two topological spaces is continuous if and only if the image under the function of every left-infinite right-closed interval is a closed set.
|
Topology.IsLower.isLowerSet_of_isOpen
theorem Topology.IsLower.isLowerSet_of_isOpen :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLower α] {s : Set α},
IsOpen s → IsLowerSet s
This theorem is stating that for any type `α` that has an inherent preorder, is endowed with a topological space structure, and has a lower topology, then any set `s` of this type that is open in this topological space is also a lower set.
In more detail, if `s` is a set in a preordered type `α` that also has a topological structure and a lower topology, and if `s` is open in this topology, then `s` has the property that for any elements `a` and `b` in `α`, if `b` is less than or equal to `a` and `a` is in `s`, then `b` is also in `s`. This defines `s` as a lower set.
More concisely: If `α` is a preordered type with a topological structure and lower topology, and `s` is an open set in `α`, then `s` is a lower set.
|
Topology.IsLower.continuous_of_Ici
theorem Topology.IsLower.continuous_of_Ici :
∀ {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLower α]
[inst_3 : TopologicalSpace β] {f : β → α}, (∀ (a : α), IsClosed (f ⁻¹' Set.Ici a)) → Continuous f
This theorem states that for any types `α` and `β`, if `α` is a preordered type with a lower topology and `β` has a topological space structure, then a function `f` from `β` to `α` is continuous if the preimage of every right-infinite interval `Set.Ici a` (which denotes the set of all elements `x` such that `a ≤ x`) is a closed set.
More concisely: A function between a preordered type with lower topology and a topological space is continuous if and only if the image under the function of every right-infinite interval is a closed set.
|
Topology.IsLower.topology_eq
theorem Topology.IsLower.topology_eq :
∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLower α],
inst_1 = Topology.lower α
This theorem states that for any type `α` that has a preorder relation and is equipped with both a topological space structure and a lower topology, the topological space structure is equivalent to the lower topology on `α`. In other words, given the type `α` and the specific structures, we can consider its existing topology as the lower topology, which is the topology generated by the complements of the left-closed right-infinite intervals.
More concisely: For any type `α` with a preorder relation and equipped with both a topology and its generated lower topology, the two topologies are equivalent.
|
Topology.IsLower.isClosed_upperClosure
theorem Topology.IsLower.isClosed_upperClosure :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLower α] {s : Set α},
s.Finite → IsClosed ↑(upperClosure s)
The theorem states that for any given finite set `s` in a preordered type `α`, which also goes along with a topological space structure and a lower topology, the upper closure of `s` is a closed set in this topological space. Here, the upper closure of a set `s` is defined as the set of all elements that are greater than or equal to at least one element in `s`. The concept of a set being "closed" is a term from topology which informally means that the set includes all its limit points.
More concisely: For any finite set `s` in a preordered type `α` with a topology and a lower topology, the upper closure of `s` is a closed set in `α`.
|
Topology.IsUpper.isUpperSet_of_isOpen
theorem Topology.IsUpper.isUpperSet_of_isOpen :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpper α] {s : Set α},
IsOpen s → IsUpperSet s
The theorem `Topology.IsUpper.isUpperSet_of_isOpen` states that every open set in the upper topology is also an upper set. More specifically, given an ordered set `α` with a preorder structure, a topological space structure, and an upper topology structure, for every subset `s` of `α`, if `s` is open in the given topological space, then `s` is also an upper set. An upper set is a set where every element that is greater than any of its members is also a member of the set. This theorem is essentially a property that relates the concepts of upper sets and open sets in the context of upper topologies.
More concisely: Every open set in an upper topology is an upper set.
|
Topology.IsUpper.continuous_of_Iic
theorem Topology.IsUpper.continuous_of_Iic :
∀ {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsUpper α]
[inst_3 : TopologicalSpace β] {f : β → α}, (∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)) → Continuous f
This theorem asserts that for any function `f` which maps from type `β` to type `α`, where `α` has a upper topology and a preorder structure, and `β` has a topological structure, if the preimage of every left-infinite right-closed interval `Set.Iic a` under this function is a closed set, then the function `f` is continuous. Here, `Set.Iic a` represents the set of all elements in `α` that are less than or equal to `a`. The upper topology on `α` is a particular way of defining what open sets are in `α`, which in this case is related to the preorder structure on `α`.
More concisely: If `f: β → α` maps `Set.Iic a` to a closed set for every `a` in `α` with an upper topology and `β` having a topological structure, then `f` is continuous.
|
Topology.IsLower.closure_singleton
theorem Topology.IsLower.closure_singleton :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLower α] (a : α),
closure {a} = Set.Ici a
This theorem states that for any given type `α` with a preorder and a lower topology, the closure of a singleton set `{a}` is the left-closed, right-infinite interval `[a, ∞)`. In other words, in the lower topology, the smallest closed set containing a single element `a` is the set of all elements `x` such that `a` is less than or equal to `x`.
More concisely: Given a type `α` with a preorder and a lower topology, the closure of a singleton set `{a}` equals the left-closed, right-infinite interval `[a, ∞)` in the lower topology.
|
Topology.IsLower.continuous_iff_Ici
theorem Topology.IsLower.continuous_iff_Ici :
∀ {α : Type u_2} {β : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsLower α]
[inst_3 : TopologicalSpace β] {f : β → α}, Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Ici a)
The theorem `Topology.IsLower.continuous_iff_Ici` states that for any types `α` and `β`, given a preorder on `α`, topological spaces on both `α` and `β`, and a lower topology on `α`, a function `f` from `β` to `α` is continuous if and only if the preimage of every left-closed right-infinite interval `Set.Ici a` under `f` is a closed set in `β`. This theorem provides a characterization of continuity in terms of preimages of intervals, specifically in the context of lower topologies.
More concisely: A function between two topological spaces is continuous with respect to a lower topology if and only if the preimage of every right-infinite, left-closed interval is a closed set.
|