mathlib3 documentation

topology.category.Born

The category of bornologies #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines Born, the category of bornologies.

@[protected, instance]
Equations
def Born.of (α : Type u_1) [bornology α] :

Construct a bundled Born from a bornology.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations