Documentation

Mathlib.Topology.Category.Born

The category of bornologies #

This defines Born, the category of bornologies.

def Born :
Type (u_1 + 1)

The category of bornologies.

Equations
Instances For
    Equations
    instance Born.instBornologyα (X : Born) :
    Equations
    • X.instBornologyα = X.str
    def Born.of (α : Type u_1) [Bornology α] :

    Construct a bundled Born from a Bornology.

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.