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.

Instances For
    def Born.of (α : Type u_1) [Bornology α] :

    Construct a bundled Born from a Bornology.

    Instances For