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.

Equations

• Topology.lawson α = Topology.lower α ⊓ Topology.scott α Set.univ

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✝ = Topology.lawson α

theorem Topology.IsLawson.topology_eq_lawson {α : Type u_1} : ∀ {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : Topology.IsLawson α], inst_1 = Topology.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.

Equations

• Topology.IsLawson.lawsonBasis α = {s : Set α | ∃ (t : Set α), t.Finite ∧ ∃ (u : Set α), IsOpen u ∧ u \ ↑(upperClosure t) = s}

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

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

Type synonym for a preorder equipped with the Lawson topology.

Equations

• Topology.WithLawson α = α

@[match_pattern]

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

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

Equations

• Topology.WithLawson.toLawson = Equiv.refl α

@[match_pattern]

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

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

Equations

• Topology.WithLawson.ofLawson = Equiv.refl (Topology.WithLawson α)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A recursor for WithLawson. Use as induction' x.

Equations

• Topology.WithLawson.rec h a = h (Topology.WithLawson.ofLawson a)

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

Equations

• ⋯ = inst

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

Equations

• Topology.WithLawson.instInhabited = inst

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

Equations

• Topology.WithLawson.instPreorder = inst

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

Equations

• Topology.WithLawson.instTopologicalSpace = Topology.lawson α

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

Equations

• ⋯ = ⋯

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

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

Equations

• Topology.WithLawson.homeomorph = Topology.WithLawson.ofLawson.toHomeomorphOfIsInducing ⋯

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

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

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

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

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

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

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

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

theorem Topology.lawsonOpen_iff_scottOpen_of_isUpperSet {α : Type u_1} [Preorder α] {s : Set α} (h : IsUpperSet s) : IsOpen (⇑Topology.WithLawson.ofLawson ⁻¹' s) ↔ IsOpen (⇑Topology.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 : TopologicalSpace α) (S : TopologicalSpace α) [Topology.IsLawson α] [Topology.IsScott α Set.univ] : L ≤ S

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

theorem Topology.lawsonOpen_iff_scottOpen_of_isUpperSet' {α : Type u_1} [Preorder α] (L : TopologicalSpace α) (S : TopologicalSpace α) [Topology.IsLawson α] [Topology.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 : TopologicalSpace α) (S : TopologicalSpace α) [Topology.IsLawson α] [Topology.IsScott α Set.univ] (s : Set α) (h : IsLowerSet s) : IsClosed s ↔ IsClosed s

theorem Topology.lawsonClosed_iff_dirSupClosed_of_isLowerSet {α : Type u_1} [Preorder α] (L : TopologicalSpace α) (S : TopologicalSpace α) [Topology.IsLawson α] [Topology.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

theorem Topology.IsLawson.singleton_isClosed {α : Type u_1} [PartialOrder α] [TopologicalSpace α] [Topology.IsLawson α] (a : α) : IsClosed {a}

@[instance 90]

instance Topology.IsLawson.t0Space {α : Type u_1} [PartialOrder α] [TopologicalSpace α] [Topology.IsLawson α] : T0Space α

The Lawson topology on a partial order is T₀.

Equations

• ⋯ = ⋯