Theorems · Definition · general topology

CompactlyGenerated.of

(X : Type w) → [inst : TopologicalSpace X] → [UCompactlyGeneratedSpace X] → CompactlyGenerated

Constructor for objects of the category CompactlyGenerated.

Defined in

Mathlib.Topology.Category.CompactlyGenerated

Cited by

2 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

TopologicalSpaceUCompactlyGeneratedSpace