Documentation

Mathlib.Topology.Category.Born

The category of bornologies #

This defines Born, the category of bornologies.

source
structure Born :
Type (u_1 + 1)

The category of bornologies.

Instances For
    source
    instance Born.instCoeSortType :
    CoeSort Born (Type u_1)
    Equations
      source
      @[reducible, inline]
      abbrev Born.of (α : Type u_1) [Bornology α] :
      Born

      Construct a bundled Born from a Bornology.

      Equations
        Instances For
          source
          instance Born.instInhabited :
          Inhabited Born
          Equations
            source
            instance Born.instLargeCategory :
            CategoryTheory.LargeCategory Born
            Equations
              source
              instance Born.instConcreteCategoryLocallyBoundedMapCarrier :
              CategoryTheory.ConcreteCategory Born fun (x1 x2 : Born) => LocallyBoundedMap x1.carrier x2.carrier
              Equations