Documentation

Mathlib.Topology.Category.Born

The category of bornologies #

This defines Born, the category of bornologies.

structure Born :

Type (u_1 + 1)

The category of bornologies.

of :: (

carrier : Type u_1
The underlying bornology.
str : Bornology self.carrier

)

Instances For

instance Born.instCoeSortType :

CoeSort Born (Type u_1)

Equations

Born.instCoeSortType = { coe := Born.carrier }

instance Born.instInhabited :

Equations

Born.instInhabited = { default := { carrier := PUnit.{?u.2 + 1}, str := instBornologyPUnit } }

instance Born.instLargeCategory :

CategoryTheory.LargeCategory Born

Equations

One or more equations did not get rendered due to their size.

instance Born.instConcreteCategoryLocallyBoundedMapCarrier :

CategoryTheory.ConcreteCategory Born fun (x1 x2 : Born) => LocallyBoundedMap x1.carrier x2.carrier

Equations

One or more equations did not get rendered due to their size.