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) [Preorder α] : TopologicalSpace α

Topology whose open sets are upper sets.

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

Equations

• Topology.upperSet α = { IsOpen := IsUpperSet, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

def Topology.lowerSet (α : Type u_4) [Preorder α] : TopologicalSpace α

Topology whose open sets are lower sets.

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

Equations

• Topology.lowerSet α = { IsOpen := IsLowerSet, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

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

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

Equations

• Topology.WithUpperSet α = α

@[match_pattern]

def Topology.WithUpperSet.toUpperSet {α : Type u_1} : α ≃ WithUpperSet α

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

Equations

• Topology.WithUpperSet.toUpperSet = Equiv.refl α

@[match_pattern]

def Topology.WithUpperSet.ofUpperSet {α : Type u_1} : WithUpperSet α ≃ α

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

Equations

• Topology.WithUpperSet.ofUpperSet = Equiv.refl (Topology.WithUpperSet α)

@[simp]

theorem Topology.WithUpperSet.toUpperSet_symm {α : Type u_1} : toUpperSet.symm = ofUpperSet

@[deprecated Topology.WithUpperSet.toUpperSet_symm (since := "2024-10-10")]

theorem Topology.WithUpperSet.to_WithUpperSet_symm_eq {α : Type u_1} : toUpperSet.symm = ofUpperSet

Alias of Topology.WithUpperSet.toUpperSet_symm.

@[simp]

theorem Topology.WithUpperSet.ofUpperSet_symm {α : Type u_1} : ofUpperSet.symm = toUpperSet

@[deprecated Topology.WithUpperSet.ofUpperSet_symm (since := "2024-10-10")]

theorem Topology.WithUpperSet.of_WithUpperSet_symm_eq {α : Type u_1} : ofUpperSet.symm = toUpperSet

Alias of Topology.WithUpperSet.ofUpperSet_symm.

@[simp]

theorem Topology.WithUpperSet.toUpperSet_ofUpperSet {α : Type u_1} (a : WithUpperSet α) : toUpperSet (ofUpperSet a) = a

@[simp]

theorem Topology.WithUpperSet.ofUpperSet_toUpperSet {α : Type u_1} (a : α) : ofUpperSet (toUpperSet a) = a

theorem Topology.WithUpperSet.toUpperSet_inj {α : Type u_1} {a b : α} : toUpperSet a = toUpperSet b ↔ a = b

theorem Topology.WithUpperSet.ofUpperSet_inj {α : Type u_1} {a b : WithUpperSet α} : ofUpperSet a = ofUpperSet b ↔ a = b

def Topology.WithUpperSet.rec {α : Type u_1} {β : WithUpperSet α → Sort u_4} (h : (a : α) → β (toUpperSet a)) (a : WithUpperSet α) : β a

A recursor for WithUpperSet. Use as induction x.

Equations

• Topology.WithUpperSet.rec h a = h (Topology.WithUpperSet.ofUpperSet a)

instance Topology.WithUpperSet.instNonempty {α : Type u_1} [Nonempty α] : Nonempty (WithUpperSet α)

instance Topology.WithUpperSet.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (WithUpperSet α)

Equations

• Topology.WithUpperSet.instInhabited = inst✝

instance Topology.WithUpperSet.instPreorder {α : Type u_1} [Preorder α] : Preorder (WithUpperSet α)

Equations

• Topology.WithUpperSet.instPreorder = inst✝

instance Topology.WithUpperSet.instTopologicalSpace {α : Type u_1} [Preorder α] : TopologicalSpace (WithUpperSet α)

Equations

• Topology.WithUpperSet.instTopologicalSpace = Topology.upperSet α

theorem Topology.WithUpperSet.ofUpperSet_le_iff {α : Type u_1} [Preorder α] {a b : WithUpperSet α} : ofUpperSet a ≤ ofUpperSet b ↔ a ≤ b

theorem Topology.WithUpperSet.toUpperSet_le_iff {α : Type u_1} [Preorder α] {a b : α} : toUpperSet a ≤ toUpperSet b ↔ a ≤ b

def Topology.WithUpperSet.ofUpperSetOrderIso {α : Type u_1} [Preorder α] : WithUpperSet α ≃o α

ofUpperSet as an OrderIso

Equations

• Topology.WithUpperSet.ofUpperSetOrderIso = { toEquiv := Topology.WithUpperSet.ofUpperSet, map_rel_iff' := ⋯ }

def Topology.WithUpperSet.toUpperSetOrderIso {α : Type u_1} [Preorder α] : α ≃o WithUpperSet α

toUpperSet as an OrderIso

Equations

• Topology.WithUpperSet.toUpperSetOrderIso = { toEquiv := Topology.WithUpperSet.toUpperSet, map_rel_iff' := ⋯ }

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

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

Equations

• Topology.WithLowerSet α = α

@[match_pattern]

def Topology.WithLowerSet.toLowerSet {α : Type u_1} : α ≃ WithLowerSet α

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

Equations

• Topology.WithLowerSet.toLowerSet = Equiv.refl α

@[match_pattern]

def Topology.WithLowerSet.ofLowerSet {α : Type u_1} : WithLowerSet α ≃ α

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

Equations

• Topology.WithLowerSet.ofLowerSet = Equiv.refl (Topology.WithLowerSet α)

@[simp]

theorem Topology.WithLowerSet.toLowerSet_symm {α : Type u_1} : toLowerSet.symm = ofLowerSet

@[deprecated Topology.WithLowerSet.toLowerSet_symm (since := "2024-10-10")]

theorem Topology.WithLowerSet.to_WithLowerSet_symm_eq {α : Type u_1} : toLowerSet.symm = ofLowerSet

Alias of Topology.WithLowerSet.toLowerSet_symm.

@[simp]

theorem Topology.WithLowerSet.ofLowerSet_symm {α : Type u_1} : ofLowerSet.symm = toLowerSet

@[deprecated Topology.WithLowerSet.ofLowerSet_symm (since := "2024-10-10")]

theorem Topology.WithLowerSet.of_WithLowerSet_symm_eq {α : Type u_1} : ofLowerSet.symm = toLowerSet

Alias of Topology.WithLowerSet.ofLowerSet_symm.

@[simp]

theorem Topology.WithLowerSet.toLowerSet_ofLowerSet {α : Type u_1} (a : WithLowerSet α) : toLowerSet (ofLowerSet a) = a

@[simp]

theorem Topology.WithLowerSet.ofLowerSet_toLowerSet {α : Type u_1} (a : α) : ofLowerSet (toLowerSet a) = a

theorem Topology.WithLowerSet.toLowerSet_inj {α : Type u_1} {a b : α} : toLowerSet a = toLowerSet b ↔ a = b

theorem Topology.WithLowerSet.ofLowerSet_inj {α : Type u_1} {a b : WithLowerSet α} : ofLowerSet a = ofLowerSet b ↔ a = b

def Topology.WithLowerSet.rec {α : Type u_1} {β : WithLowerSet α → Sort u_4} (h : (a : α) → β (toLowerSet a)) (a : WithLowerSet α) : β a

A recursor for WithLowerSet. Use as induction x.

Equations

• Topology.WithLowerSet.rec h a = h (Topology.WithLowerSet.ofLowerSet a)

instance Topology.WithLowerSet.instNonempty {α : Type u_1} [Nonempty α] : Nonempty (WithLowerSet α)

instance Topology.WithLowerSet.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (WithLowerSet α)

Equations

• Topology.WithLowerSet.instInhabited = inst✝

instance Topology.WithLowerSet.instPreorder {α : Type u_1} [Preorder α] : Preorder (WithLowerSet α)

Equations

• Topology.WithLowerSet.instPreorder = inst✝

instance Topology.WithLowerSet.instTopologicalSpace {α : Type u_1} [Preorder α] : TopologicalSpace (WithLowerSet α)

Equations

• Topology.WithLowerSet.instTopologicalSpace = Topology.lowerSet α

theorem Topology.WithLowerSet.ofLowerSet_le_iff {α : Type u_1} [Preorder α] {a b : WithLowerSet α} : ofLowerSet a ≤ ofLowerSet b ↔ a ≤ b

theorem Topology.WithLowerSet.toLowerSet_le_iff {α : Type u_1} [Preorder α] {a b : α} : toLowerSet a ≤ toLowerSet b ↔ a ≤ b

def Topology.WithLowerSet.ofLowerSetOrderIso {α : Type u_1} [Preorder α] : WithLowerSet α ≃o α

ofLowerSet as an OrderIso

Equations

• Topology.WithLowerSet.ofLowerSetOrderIso = { toEquiv := Topology.WithLowerSet.ofLowerSet, map_rel_iff' := ⋯ }

def Topology.WithLowerSet.toLowerSetOrderIso {α : Type u_1} [Preorder α] : α ≃o WithLowerSet α

toLowerSet as an OrderIso

Equations

• Topology.WithLowerSet.toLowerSetOrderIso = { toEquiv := Topology.WithLowerSet.toLowerSet, map_rel_iff' := ⋯ }

def Topology.WithUpperSet.toDualHomeomorph {α : Type u_1} [Preorder α] : WithUpperSet α ≃ₜ WithLowerSet αᵒᵈ

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

Equations

• Topology.WithUpperSet.toDualHomeomorph = { toFun := ⇑OrderDual.toDual, invFun := ⇑OrderDual.ofDual, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

class Topology.IsUpperSet (α : Type u_4) [t : TopologicalSpace α] [Preorder α] : Prop

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.

• topology_eq_upperSetTopology : t = upperSet α

instance Topology.instIsUpperSetWithUpperSet {α : Type u_1} [Preorder α] : Topology.IsUpperSet (WithUpperSet α)

instance Topology.instIsUpperSet {α : Type u_1} [Preorder α] : Topology.IsUpperSet α

class Topology.IsLowerSet (α : Type u_4) [t : TopologicalSpace α] [Preorder α] : Prop

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.

• topology_eq_lowerSetTopology : t = lowerSet α

instance Topology.instIsLowerSetWithLowerSet {α : Type u_1} [Preorder α] : Topology.IsLowerSet (WithLowerSet α)

instance Topology.instIsLowerSet {α : Type u_1} [Preorder α] : Topology.IsLowerSet α

theorem Topology.IsUpperSet.topology_eq (α : Type u_1) [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] : inst✝ = upperSet α

instance OrderDual.instIsLowerSet {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] : Topology.IsLowerSet αᵒᵈ

def Topology.IsUpperSet.WithUpperSetHomeomorph {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] : WithUpperSet α ≃ₜ α

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

Equations

• Topology.IsUpperSet.WithUpperSetHomeomorph = Topology.WithUpperSet.ofUpperSet.toHomeomorphOfIsInducing ⋯

theorem Topology.IsUpperSet.isOpen_iff_isUpperSet {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] {s : Set α} : IsOpen s ↔ IsUpperSet s

instance Topology.IsUpperSet.toAlexandrovDiscrete {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] : AlexandrovDiscrete α

theorem Topology.IsUpperSet.isClosed_iff_isLower {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] {s : Set α} : IsClosed s ↔ IsLowerSet s

theorem Topology.IsUpperSet.closure_eq_lowerClosure {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] {s : Set α} : closure s = ↑(lowerClosure s)

@[simp]

theorem Topology.IsUpperSet.closure_singleton {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] {a : α} : closure {a} = Set.Iic 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} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [Topology.IsUpperSet α] [Topology.IsUpperSet β] {f : α → β} : Monotone f ↔ Continuous f

theorem Topology.IsUpperSet.monotone_to_upperTopology_continuous {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [Topology.IsUpperSet α] [IsUpper β] {f : α → β} (hf : Monotone f) : Continuous f

theorem Topology.IsUpperSet.upperSet_le_upper {α : Type u_1} [Preorder α] {t₁ t₂ : TopologicalSpace α} [Topology.IsUpperSet α] [IsUpper α] : t₁ ≤ t₂

theorem Topology.IsLowerSet.topology_eq (α : Type u_1) [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] : inst✝ = lowerSet α

instance OrderDual.instIsUpperSet {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] : Topology.IsUpperSet αᵒᵈ

def Topology.IsLowerSet.WithLowerSetHomeomorph {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] : WithLowerSet α ≃ₜ α

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

Equations

• Topology.IsLowerSet.WithLowerSetHomeomorph = Topology.WithLowerSet.ofLowerSet.toHomeomorphOfIsInducing ⋯

theorem Topology.IsLowerSet.isOpen_iff_isLowerSet {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {s : Set α} : IsOpen s ↔ IsLowerSet s

instance Topology.IsLowerSet.toAlexandrovDiscrete {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] : AlexandrovDiscrete α

theorem Topology.IsLowerSet.isClosed_iff_isUpper {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {s : Set α} : IsClosed s ↔ IsUpperSet s

theorem Topology.IsLowerSet.closure_eq_upperClosure {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {s : Set α} : closure s = ↑(upperClosure s)

@[simp]

theorem Topology.IsLowerSet.closure_singleton {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {a : α} : closure {a} = Set.Ici 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} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [Topology.IsLowerSet α] [Topology.IsLowerSet β] {f : α → β} : Monotone f ↔ Continuous f

theorem Topology.IsLowerSet.monotone_to_lowerTopology_continuous {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [Topology.IsLowerSet α] [IsLower β] {f : α → β} (hf : Monotone f) : Continuous f

theorem Topology.IsLowerSet.lowerSet_le_lower {α : Type u_1} [Preorder α] {t₁ t₂ : TopologicalSpace α} [Topology.IsLowerSet α] [IsLower α] : t₁ ≤ t₂

theorem Topology.isUpperSet_orderDual {α : Type u_1} [Preorder α] [TopologicalSpace α] : Topology.IsUpperSet αᵒᵈ ↔ Topology.IsLowerSet α

theorem Topology.isLowerSet_orderDual {α : Type u_1} [Preorder α] [TopologicalSpace α] : Topology.IsLowerSet αᵒᵈ ↔ Topology.IsUpperSet α

def Topology.WithUpperSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) : C(WithUpperSet α, WithUpperSet β)

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

Equations

• Topology.WithUpperSet.map f = { toFun := ⇑Topology.WithUpperSet.toUpperSet ∘ ⇑f ∘ ⇑Topology.WithUpperSet.ofUpperSet, continuous_toFun := ⋯ }

@[simp]

theorem Topology.WithUpperSet.map_id {α : Type u_1} [Preorder α] : map OrderHom.id = ContinuousMap.id (WithUpperSet α)

@[simp]

theorem Topology.WithUpperSet.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) : map (g.comp f) = (map g).comp (map f)

@[simp]

theorem Topology.WithUpperSet.toUpperSet_specializes_toUpperSet {α : Type u_1} [Preorder α] {a b : α} : toUpperSet a ⤳ toUpperSet b ↔ b ≤ a

@[simp]

theorem Topology.WithUpperSet.ofUpperSet_le_ofUpperSet {α : Type u_1} [Preorder α] {a b : WithUpperSet α} : ofUpperSet a ≤ ofUpperSet b ↔ b ⤳ a

@[simp]

theorem Topology.WithUpperSet.isUpperSet_toUpperSet_preimage {α : Type u_1} [Preorder α] {s : Set (WithUpperSet α)} : IsUpperSet (⇑toUpperSet ⁻¹' s) ↔ IsOpen s

@[simp]

theorem Topology.WithUpperSet.isOpen_ofUpperSet_preimage {α : Type u_1} [Preorder α] {s : Set α} : IsOpen (⇑ofUpperSet ⁻¹' s) ↔ IsUpperSet s

def Topology.WithLowerSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) : C(WithLowerSet α, WithLowerSet β)

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

Equations

• Topology.WithLowerSet.map f = { toFun := ⇑Topology.WithLowerSet.toLowerSet ∘ ⇑f ∘ ⇑Topology.WithLowerSet.ofLowerSet, continuous_toFun := ⋯ }

@[simp]

theorem Topology.WithLowerSet.map_id {α : Type u_1} [Preorder α] : map OrderHom.id = ContinuousMap.id (WithLowerSet α)

@[simp]

theorem Topology.WithLowerSet.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] (g : β →o γ) (f : α →o β) : map (g.comp f) = (map g).comp (map f)

@[simp]

theorem Topology.WithLowerSet.toLowerSet_specializes_toLowerSet {α : Type u_1} [Preorder α] {a b : α} : toLowerSet a ⤳ toLowerSet b ↔ a ≤ b

@[simp]

theorem Topology.WithLowerSet.ofLowerSet_le_ofLowerSet {α : Type u_1} [Preorder α] {a b : WithLowerSet α} : ofLowerSet a ≤ ofLowerSet b ↔ a ⤳ b

@[simp]

theorem Topology.WithLowerSet.isLowerSet_toLowerSet_preimage {α : Type u_1} [Preorder α] {s : Set (WithLowerSet α)} : IsLowerSet (⇑toLowerSet ⁻¹' s) ↔ IsOpen s

@[simp]

theorem Topology.WithLowerSet.isOpen_ofLowerSet_preimage {α : Type u_1} [Preorder α] {s : Set α} : IsOpen (⇑ofLowerSet ⁻¹' s) ↔ IsLowerSet s