# Documentation

Mathlib.Topology.Order.UpperLowerSetTopology

# Upper and lower sets topologies #

This file introduces the upper set topology on a preorder as the topology where the open sets are the upper sets and the lower set topology on a preorder as the topology where the open sets are the lower sets.

In general the upper set topology does not coincide with the upper topology and the lower set topology does not coincide with the lower topology.

## Main statements #

• Topology.IsUpperSet.toAlexandrovDiscrete: The upper set topology is Alexandrov-discrete.
• Topology.IsUpperSet.isClosed_iff_isLower - a set is closed if and only if it is a Lower set
• Topology.IsUpperSet.closure_eq_lowerClosure - topological closure coincides with lower closure
• Topology.IsUpperSet.monotone_iff_continuous - the continuous functions are the monotone functions
• IsUpperSet.monotone_to_upperTopology_continuous: A monotone map from a preorder with the upper set topology to a preorder with the upper topology is continuous.

We provide the upper set topology in three ways (and similarly for the lower set topology):

• Topology.upperSet: The upper set topology as a TopologicalSpace α
• Topology.IsUpperSet: Prop-valued mixin typeclass stating that an existing topology is the upper set topology.
• Topology.WithUpperSet: Type synonym equipping a preorder with its upper set topology.

## Motivation #

An Alexandrov topology is a topology where the intersection of any collection of open sets is open. The upper set topology is an Alexandrov topology and, given any Alexandrov topological space, we can equip it with a preorder (namely the specialization preorder) whose upper set topology coincides with the original topology. See Topology.Specialization.

## Tags #

upper set topology, lower set topology, preorder, Alexandrov

def Topology.upperSet (α : Type u_4) [] :

Topology whose open sets are upper sets.

Note: In general the upper set topology does not coincide with the upper topology.

Instances For
def Topology.lowerSet (α : Type u_4) [] :

Topology whose open sets are lower sets.

Note: In general the lower set topology does not coincide with the lower topology.

Instances For
def Topology.WithUpperSet (α : Type u_4) :
Type u_4

Type synonym for a preorder equipped with the upper set topology.

Instances For
@[match_pattern]

toUpperSet is the identity function to the WithUpperSet of a type.

Instances For
@[match_pattern]

ofUpperSet is the identity function from the WithUpperSet of a type.

Instances For
@[simp]
theorem Topology.WithUpperSet.to_WithUpperSet_symm_eq {α : Type u_1} :
Topology.WithUpperSet.toUpperSet.symm = Topology.WithUpperSet.ofUpperSet
@[simp]
theorem Topology.WithUpperSet.of_WithUpperSet_symm_eq {α : Type u_1} :
Topology.WithUpperSet.ofUpperSet.symm = Topology.WithUpperSet.toUpperSet
@[simp]
theorem Topology.WithUpperSet.toUpperSet_ofUpperSet {α : Type u_1} (a : ) :
Topology.WithUpperSet.toUpperSet (Topology.WithUpperSet.ofUpperSet a) = a
@[simp]
theorem Topology.WithUpperSet.ofUpperSet_toUpperSet {α : Type u_1} (a : α) :
Topology.WithUpperSet.ofUpperSet (Topology.WithUpperSet.toUpperSet a) = a
theorem Topology.WithUpperSet.toUpperSet_inj {α : Type u_1} {a : α} {b : α} :
Topology.WithUpperSet.toUpperSet a = Topology.WithUpperSet.toUpperSet b a = b
theorem Topology.WithUpperSet.ofUpperSet_inj {α : Type u_1} {a : } {b : } :
Topology.WithUpperSet.ofUpperSet a = Topology.WithUpperSet.ofUpperSet b a = b
def Topology.WithUpperSet.rec {α : Type u_1} {β : } (h : (a : α) → β (Topology.WithUpperSet.toUpperSet a)) (a : ) :
β a

A recursor for WithUpperSet. Use as induction x using WithUpperSet.rec.

Instances For
theorem Topology.WithUpperSet.ofUpperSet_le_iff {α : Type u_1} [] {a : } {b : } :
Topology.WithUpperSet.ofUpperSet a Topology.WithUpperSet.ofUpperSet b a b
theorem Topology.WithUpperSet.toUpperSet_le_iff {α : Type u_1} [] {a : α} {b : α} :
Topology.WithUpperSet.toUpperSet a Topology.WithUpperSet.toUpperSet b a b

ofUpperSet as an OrderIso

Instances For

toUpperSet as an OrderIso

Instances For
def Topology.WithLowerSet (α : Type u_4) :
Type u_4

Type synonym for a preorder equipped with the lower set topology.

Instances For
@[match_pattern]

toLowerSet is the identity function to the WithLowerSet of a type.

Instances For
@[match_pattern]

ofLowerSet is the identity function from the WithLowerSet of a type.

Instances For
@[simp]
theorem Topology.WithLowerSet.to_WithLowerSet_symm_eq {α : Type u_1} :
Topology.WithLowerSet.toLowerSet.symm = Topology.WithLowerSet.ofLowerSet
@[simp]
theorem Topology.WithLowerSet.of_WithLowerSet_symm_eq {α : Type u_1} :
Topology.WithLowerSet.ofLowerSet.symm = Topology.WithLowerSet.toLowerSet
@[simp]
theorem Topology.WithLowerSet.toLowerSet_ofLowerSet {α : Type u_1} (a : ) :
Topology.WithLowerSet.toLowerSet (Topology.WithLowerSet.ofLowerSet a) = a
@[simp]
theorem Topology.WithLowerSet.ofLowerSet_toLowerSet {α : Type u_1} (a : α) :
Topology.WithLowerSet.ofLowerSet (Topology.WithLowerSet.toLowerSet a) = a
theorem Topology.WithLowerSet.toLowerSet_inj {α : Type u_1} {a : α} {b : α} :
Topology.WithLowerSet.toLowerSet a = Topology.WithLowerSet.toLowerSet b a = b
theorem Topology.WithLowerSet.ofLowerSet_inj {α : Type u_1} {a : } {b : } :
Topology.WithLowerSet.ofLowerSet a = Topology.WithLowerSet.ofLowerSet b a = b
def Topology.WithLowerSet.rec {α : Type u_1} {β : } (h : (a : α) → β (Topology.WithLowerSet.toLowerSet a)) (a : ) :
β a

A recursor for WithLowerSet. Use as induction x using WithLowerSet.rec.

Instances For
theorem Topology.WithLowerSet.ofLowerSet_le_iff {α : Type u_1} [] {a : } {b : } :
Topology.WithLowerSet.ofLowerSet a Topology.WithLowerSet.ofLowerSet b a b
theorem Topology.WithLowerSet.toLowerSet_le_iff {α : Type u_1} [] {a : α} {b : α} :
Topology.WithLowerSet.toLowerSet a Topology.WithLowerSet.toLowerSet b a b

ofLowerSet as an OrderIso

Instances For

toLowerSet as an OrderIso

Instances For

The Upper Set topology is homeomorphic to the Lower Set topology on the dual order

Instances For
class Topology.IsUpperSet (α : Type u_4) [t : ] [] :
• topology_eq_upperSetTopology :

Prop-valued mixin for an ordered topological space to be The upper set topology is the topology where the open sets are the upper sets. In general the upper set topology does not coincide with the upper topology.

Instances
class Topology.IsLowerSet (α : Type u_4) [t : ] [] :
• topology_eq_lowerSetTopology :

The lower set topology is the topology where the open sets are the lower sets. In general the lower set topology does not coincide with the lower topology.

Instances
theorem Topology.IsUpperSet.topology_eq (α : Type u_1) [] [] :
inst✝ =
instance OrderDual.instIsLowerSet {α : Type u_1} [] [] :

If α is equipped with the upper set topology, then it is homeomorphic to WithUpperSet α.

Instances For
theorem Topology.IsUpperSet.isOpen_iff_isUpperSet {α : Type u_1} [] [] {s : Set α} :
theorem Topology.IsUpperSet.isClosed_iff_isLower {α : Type u_1} [] [] {s : Set α} :
theorem Topology.IsUpperSet.closure_eq_lowerClosure {α : Type u_1} [] [] {s : Set α} :
= ↑()
@[simp]
theorem Topology.IsUpperSet.closure_singleton {α : Type u_1} [] [] {a : α} :
closure {a} =

The closure of a singleton {a} in the upper set topology is the right-closed left-infinite interval (-∞,a].

theorem Topology.IsUpperSet.monotone_iff_continuous {α : Type u_1} {β : Type u_2} [] [] [] [] {f : αβ} :
theorem Topology.IsUpperSet.monotone_to_upperTopology_continuous {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} (hf : ) :
theorem Topology.IsUpperSet.upperSet_le_upper {α : Type u_1} [] {t₁ : } {t₂ : } [] :
t₁ t₂
theorem Topology.IsLowerSet.topology_eq (α : Type u_1) [] [] :
inst✝ =
instance OrderDual.instIsUpperSet {α : Type u_1} [] [] :

If α is equipped with the lower set topology, then it is homeomorphic to WithLowerSet α.

Instances For
theorem Topology.IsLowerSet.isOpen_iff_isLowerSet {α : Type u_1} [] [] {s : Set α} :
theorem Topology.IsLowerSet.isClosed_iff_isUpper {α : Type u_1} [] [] {s : Set α} :
theorem Topology.IsLowerSet.closure_eq_upperClosure {α : Type u_1} [] [] {s : Set α} :
= ↑()
@[simp]
theorem Topology.IsLowerSet.closure_singleton {α : Type u_1} [] [] {a : α} :
closure {a} =

The closure of a singleton {a} in the lower set topology is the right-closed left-infinite interval (-∞,a].

theorem Topology.IsLowerSet.monotone_iff_continuous {α : Type u_1} {β : Type u_2} [] [] [] [] {f : αβ} :
theorem Topology.IsLowerSet.monotone_to_lowerTopology_continuous {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} (hf : ) :
theorem Topology.IsLowerSet.lowerSet_le_lower {α : Type u_1} [] {t₁ : } {t₂ : } [] :
t₁ t₂
theorem Topology.isUpperSet_orderDual {α : Type u_1} [] [] :
theorem Topology.isLowerSet_orderDual {α : Type u_1} [] [] :
def Topology.WithUpperSet.map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) :

A monotone map between preorders spaces induces a continuous map between themselves considered with the upper set topology.

Instances For
@[simp]
theorem Topology.WithUpperSet.map_id {α : Type u_1} [] :
@[simp]
theorem Topology.WithUpperSet.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : β →o γ) (f : α →o β) :
@[simp]
theorem Topology.WithUpperSet.toUpperSet_specializes_toUpperSet {α : Type u_1} [] {a : α} {b : α} :
Topology.WithUpperSet.toUpperSet a Topology.WithUpperSet.toUpperSet b b a
@[simp]
theorem Topology.WithUpperSet.ofUpperSet_le_ofUpperSet {α : Type u_1} [] {a : } {b : } :
Topology.WithUpperSet.ofUpperSet a Topology.WithUpperSet.ofUpperSet b b a
@[simp]
theorem Topology.WithUpperSet.isUpperSet_toUpperSet_preimage {α : Type u_1} [] {s : } :
IsUpperSet (Topology.WithUpperSet.toUpperSet ⁻¹' s)
@[simp]
theorem Topology.WithUpperSet.isOpen_ofUpperSet_preimage {α : Type u_1} [] {s : Set α} :
IsOpen (Topology.WithUpperSet.ofUpperSet ⁻¹' s)
def Topology.WithLowerSet.map {α : Type u_1} {β : Type u_2} [] [] (f : α →o β) :

A monotone map between preorders spaces induces a continuous map between themselves considered with the lower set topology.

Instances For
@[simp]
theorem Topology.WithLowerSet.map_id {α : Type u_1} [] :
@[simp]
theorem Topology.WithLowerSet.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : β →o γ) (f : α →o β) :
@[simp]
theorem Topology.WithLowerSet.toLowerSet_specializes_toLowerSet {α : Type u_1} [] {a : α} {b : α} :
Topology.WithLowerSet.toLowerSet a Topology.WithLowerSet.toLowerSet b a b
@[simp]
theorem Topology.WithLowerSet.ofLowerSet_le_ofLowerSet {α : Type u_1} [] {a : } {b : } :
Topology.WithLowerSet.ofLowerSet a Topology.WithLowerSet.ofLowerSet b a b
@[simp]
theorem Topology.WithLowerSet.isLowerSet_toLowerSet_preimage {α : Type u_1} [] {s : } :
IsLowerSet (Topology.WithLowerSet.toLowerSet ⁻¹' s)
@[simp]
theorem Topology.WithLowerSet.isOpen_ofLowerSet_preimage {α : Type u_1} [] {s : Set α} :
IsOpen (Topology.WithLowerSet.ofLowerSet ⁻¹' s)