Documentation

Mathlib.Topology.Category.Born

The category of bornologies #

This defines Born, the category of bornologies.

source
def Born :
Type (u_1 + 1)

The category of bornologies.

Instances For
    source
    instance Born.instCoeSortBornType :
    CoeSort Born (Type u_1)
    source
    instance Born.instBornologyα (X : Born) :
    Bornology ↑X
    source
    def Born.of (α : Type u_1) [Bornology α] :
    Born

    Construct a bundled Born from a Bornology.

    Instances For
      source
      instance Born.instInhabitedBorn :
      Inhabited Born
      source
      instance Born.instBundledHomTypeBornologyLocallyBoundedMap :
      CategoryTheory.BundledHom LocallyBoundedMap
      source
      instance Born.instLargeCategoryBorn :
      CategoryTheory.LargeCategory Born
      source
      instance Born.instConcreteCategoryBornInstLargeCategoryBorn :
      CategoryTheory.ConcreteCategory Born