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.

source
def Born  :
Type (u_1+1)

The category of bornologies.

Equations
Instances for Born
source
@[protected, instance]
def Born.has_coe_to_sort  :
has_coe_to_sort Born (Type u_1)
Equations
source
@[protected, instance]
def Born.bornology (X : Born) :
bornology ↥X
Equations
source
def Born.of (α : Type u_1) [bornology α] :
Born

Construct a bundled Born from a bornology.

Equations
source
@[protected, instance]
def Born.inhabited  :
inhabited Born
Equations
source
@[protected, instance]
def Born.locally_bounded_map.category_theory.bundled_hom  :
category_theory.bundled_hom locally_bounded_map
Equations
source
@[protected, instance]
def Born.category_theory.large_category  :
category_theory.large_category Born
Equations
source
@[protected, instance]
def Born.category_theory.concrete_category  :
category_theory.concrete_category Born
Equations