Documentation

Mathlib.Topology.Category.DeltaGenerated

Delta-generated topological spaces #

The category of delta-generated spaces.

See https://ncatlab.org/nlab/show/Delta-generated+topological+space.

Adapted from Mathlib.Topology.Category.CompactlyGenerated.

TODO #

structure DeltaGenerated :
Type (u + 1)

The type of delta-generated topological spaces.

Instances For
    @[reducible, inline]

    Constructor for objects of the category DeltaGenerated

    Equations
    Instances For

      The faithful (but not full) functor taking each topological space to its delta-generated coreflection.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The adjunction between the forgetful functor DeltaGeneratedTopCat and its coreflector.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For