Structures · Topology
UCompactlyGeneratedSpace
A topological space X is compactly generated if its topology is finer than (and thus equal to)
the compactly generated topology, i.e. it is coinduced by the continuous maps from compact
Hausdorff spaces to X.
This version includes an explicit universe parameter u which should always be specified. It is
intended for categorical purposes. See CompactlyGeneratedSpace for the version without this
parameter, intended for topological purposes.
- Shape
- One type argument · adds le_compactlyGenerated
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- TopCat.carrier
- Sum
- Sigma
- Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- CompactlyGenerated.of
- UCompactlyGeneratedSpace.isClosed
- eq_compactlyGenerated
- UCompactlyGeneratedSpace.le_compactlyGenerated
- CompactlyGenerated.ofHom
- uCompactlyGeneratedSpace_of_coinduced
- UCompactlyGeneratedSpace.isOpen
- continuous_from_uCompactlyGeneratedSpace
- CondensedSet.compactlyGeneratedAdjunctionCounitHomeo
- instUCompactlyGeneratedSpaceQuotient
- instUCompactlyGeneratedSpaceSum
- instUCompactlyGeneratedSpaceSigma
Ancestors0
No ancestors.