Lawson topology

This file introduces the Lawson topology on a preorder.

Main definitions

• Topology.lawson - the Lawson topology is defined as the meet of the lower topology and the Scott topology.
• Topology.IsLawson.lawsonBasis - The complements of the upper closures of finite sets intersected with Scott open sets.

Main statements

• Topology.IsLawson.isTopologicalBasis - Topology.IsLawson.lawsonBasis is a basis for Topology.IsLawson
• Topology.lawsonOpen_iff_scottOpen_of_isUpperSet' - An upper set is Lawson open if and only if it is Scott open
• Topology.lawsonClosed_iff_dirSupClosed_of_isLowerSet - A lower set is Lawson closed if and only if it is closed under sups of directed sets
• Topology.IsLawson.t0Space - The Lawson topology is T₀

Implementation notes

A type synonym Topology.WithLawson is introduced and for a preorder α, Topology.WithLawson α is made an instance of TopologicalSpace by Topology.lawson.

We define a mixin class Topology.IsLawson for the class of types which are both a preorder and a topology and where the topology is Topology.lawson. It is shown that Topology.WithLawson α is an instance of Topology.IsLawson.

References

• [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]

Tags

Lawson topology, preorder

Lawson topology

def Topology.lawson (α : Type u_2) [Preorder α] : TopologicalSpace α

The Lawson topology is defined as the meet of Topology.lower and the Topology.scott.

class Topology.IsLawson (α : Type u_1) [Preorder α] [TopologicalSpace α] : Prop

Predicate for an ordered topological space to be equipped with its Lawson topology.

The Lawson topology is defined as the meet of Topology.lower and the Topology.scott.

• topology_eq_lawson : inst✝ = lawson α

def Topology.IsLawson.lawsonBasis (α : Type u_1) [Preorder α] : Set (Set α)

The complements of the upper closures of finite sets intersected with Scott open sets form a basis for the lawson topology.

theorem Topology.IsLawson.isTopologicalBasis (α : Type u_1) [Preorder α] [TopologicalSpace α] [IsLawson α] : TopologicalSpace.IsTopologicalBasis (lawsonBasis α)

def Topology.WithLawson (α : Type u_2) : Type u_2

Type synonym for a preorder equipped with the Lawson topology.

@[match_pattern]

def Topology.WithLawson.toLawson {α : Type u_1} : α ≃ WithLawson α

toLawson is the identity function to the WithLawson of a type.

@[match_pattern]

def Topology.WithLawson.ofLawson {α : Type u_1} : WithLawson α ≃ α

ofLawson is the identity function from the WithLawson of a type.

@[simp]

theorem Topology.WithLawson.to_Lawson_symm_eq {α : Type u_1} : toLawson.symm = ofLawson

@[simp]

theorem Topology.WithLawson.of_Lawson_symm_eq {α : Type u_1} : ofLawson.symm = toLawson

@[simp]

theorem Topology.WithLawson.toLawson_ofLawson {α : Type u_1} (a : WithLawson α) : toLawson (ofLawson a) = a

@[simp]

theorem Topology.WithLawson.ofLawson_toLawson {α : Type u_1} (a : α) : ofLawson (toLawson a) = a

theorem Topology.WithLawson.toLawson_inj {α : Type u_1} {a b : α} : toLawson a = toLawson b ↔ a = b

theorem Topology.WithLawson.ofLawson_inj {α : Type u_1} {a b : WithLawson α} : ofLawson a = ofLawson b ↔ a = b

def Topology.WithLawson.rec {α : Type u_1} {β : WithLawson α → Sort u_2} (h : (a : α) → β (toLawson a)) (a : WithLawson α) : β a

A recursor for WithLawson. Use as induction x.

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

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

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

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

instance Topology.WithLawson.instIsLawson {α : Type u_1} [Preorder α] : IsLawson (WithLawson α)

def Topology.WithLawson.homeomorph {α : Type u_1} [Preorder α] [TopologicalSpace α] [IsLawson α] : WithLawson α ≃ₜ α

If α is equipped with the Lawson topology, then it is homeomorphic to WithLawson α.

theorem Topology.WithLawson.isOpen_preimage_ofLawson {α : Type u_1} [Preorder α] {S : Set α} : IsOpen (⇑ofLawson ⁻¹' S) ↔ TopologicalSpace.IsOpen S

theorem Topology.WithLawson.isClosed_preimage_ofLawson {α : Type u_1} [Preorder α] {S : Set α} : IsClosed (⇑ofLawson ⁻¹' S) ↔ IsClosed S

theorem Topology.WithLawson.isOpen_def {α : Type u_1} [Preorder α] {T : Set (WithLawson α)} : IsOpen T ↔ TopologicalSpace.IsOpen (⇑toLawson ⁻¹' T)

theorem Topology.lawson_le_scott {α : Type u_1} [Preorder α] : lawson α ≤ scott α Set.univ

theorem Topology.lawson_le_lower {α : Type u_1} [Preorder α] : lawson α ≤ lower α

theorem Topology.scottHausdorff_le_lawson {α : Type u_1} [Preorder α] : scottHausdorff α Set.univ ≤ lawson α

theorem Topology.lawsonClosed_of_scottClosed {α : Type u_1} [Preorder α] (s : Set α) (h : IsClosed (⇑WithScott.ofScott ⁻¹' s)) : IsClosed (⇑WithLawson.ofLawson ⁻¹' s)

theorem Topology.lawsonClosed_of_lowerClosed {α : Type u_1} [Preorder α] (s : Set α) (h : IsClosed (⇑WithLower.ofLower ⁻¹' s)) : IsClosed (⇑WithLawson.ofLawson ⁻¹' s)

theorem Topology.lawsonOpen_iff_scottOpen_of_isUpperSet {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) : IsOpen (⇑WithLawson.ofLawson ⁻¹' s) ↔ IsOpen (⇑WithScott.ofScott ⁻¹' s)

An upper set is Lawson open if and only if it is Scott open

theorem Topology.isLawson_le_isScott {α : Type u_1} [Preorder α] (L S : TopologicalSpace α) [IsLawson α] [IsScott α Set.univ] : L ≤ S

theorem Topology.scottHausdorff_le_isLawson {α : Type u_1} [Preorder α] (L : TopologicalSpace α) [IsLawson α] : scottHausdorff α Set.univ ≤ L

theorem Topology.lawsonOpen_iff_scottOpen_of_isUpperSet' {α : Type u_1} [Preorder α] (L S : TopologicalSpace α) [IsLawson α] [IsScott α Set.univ] (s : Set α) (h : IsUpperSet s) : IsOpen s ↔ IsOpen s

An upper set is Lawson open if and only if it is Scott open

theorem Topology.lawsonClosed_iff_scottClosed_of_isLowerSet {α : Type u_1} [Preorder α] (L S : TopologicalSpace α) [IsLawson α] [IsScott α Set.univ] (s : Set α) (h : IsLowerSet s) : IsClosed s ↔ IsClosed s

theorem Topology.lawsonClosed_iff_dirSupClosed_of_isLowerSet {α : Type u_1} [Preorder α] (L S : TopologicalSpace α) [IsLawson α] [IsScott α Set.univ] (s : Set α) (h : IsLowerSet s) : IsClosed s ↔ DirSupClosed s

A lower set is Lawson closed if and only if it is closed under sups of directed sets

@[instance 90]

instance Topology.IsLawson.toT1Space {α : Type u_1} [PartialOrder α] [TopologicalSpace α] [IsLawson α] : T1Space α

The Lawson topology on a partial order is T₁.

@[deprecated isClosed_singleton (since := "2025-07-02")]

theorem Topology.IsLawson.singleton_isClosed {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} : IsClosed {x}

Alias of isClosed_singleton.