mathlib3 documentation

topology.order.lower_topology

Lower topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file introduces the lower topology on a preorder as the topology generated by the complements of the closed intervals to infinity.

Main statements #

Implementation notes #

A type synonym with_lower_topology is introduced and for a preorder α, with_lower_topology α is made an instance of topological_space by the topology generated by the complements of the closed intervals to infinity.

We define a mixin class lower_topology for the class of types which are both a preorder and a topology and where the topology is generated by the complements of the closed intervals to infinity. It is shown that with_lower_topology α is an instance of lower_topology.

Motivation #

The lower topology is used with the Scott topology to define the Lawson topology. The restriction of the lower topology to the spectrum of a complete lattice coincides with the hull-kernel topology.

References #

Tags #

lower topology, preorder

def with_lower_topology (α : Type u_1) :
Type u_1

Type synonym for a preorder equipped with the lower topology

Equations
Instances for with_lower_topology

to_lower is the identity function to the with_lower_topology of a type.

Equations

of_lower is the identity function from the with_lower_topology of a type.

Equations
@[protected]
def with_lower_topology.rec {α : Type u_1} {β : with_lower_topology α Sort u_2} (h : Π (a : α), β (with_lower_topology.to_lower a)) (a : with_lower_topology α) :
β a

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

Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[class]
structure lower_topology (α : Type u_3) [t : topological_space α] [preorder α] :
Prop

The lower topology is the topology generated by the complements of the closed intervals to infinity.

Instances of this typeclass
@[protected, instance]
def lower_topology.lower_basis (α : Type u_1) [preorder α] :
set (set α)

The complements of the upper closures of finite sets are a collection of lower sets which form a basis for the lower topology.

Equations
theorem lower_topology.is_closed_Ici {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] (a : α) :

Left-closed right-infinite intervals [a, ∞) are closed in the lower topology.

The upper closure of a finite set is closed in the lower topology.

Every set open in the lower topology is a lower set.

@[simp]
theorem lower_topology.closure_singleton {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] (a : α) :

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

@[protected, instance]

The lower topology on a partial order is T₀.

@[protected, instance]