Documentation

Mathlib.Topology.Category.Born

The category of bornologies #

This defines Born, the category of bornologies.

source
🔶 coverage
structure Born :
Type (u_1 + 1)

The category of bornologies.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance Born.instCoeSortType :
    CoeSort Born (Type u_1)
    source
    🔸 coverage
    @[implicit_reducible]
    instance Born.instInhabited :
    Inhabited Born
    source
    🔸 coverage
    @[implicit_reducible]
    instance Born.instLargeCategory :
    CategoryTheory.LargeCategory Born
    source
    🔸 coverage
    @[implicit_reducible]
    instance Born.instConcreteCategoryLocallyBoundedMapCarrier :
    CategoryTheory.ConcreteCategory Born fun (x1 x2 : Born) => LocallyBoundedMap x1.carrier x2.carrier