Documentation

Mathlib.Topology.Category.Locale

The category of locales #

This file defines Locale, the category of locales. This is the opposite of the category of frames.

def Locale :
Type (u_1 + 1)

The category of locales.

Equations
Instances For
    Equations
    Equations
    def Locale.of (α : Type u_1) [Order.Frame α] :

    Construct a bundled Locale from a Frame.

    Equations
    Instances For
      @[simp]
      theorem Locale.coe_of (α : Type u_1) [Order.Frame α] :
      @[simp]

      The forgetful functor from Top to Locale which forgets that the space has "enough points".

      Equations
      Instances For