Theorems · Definition · category theory

CompHaus.of

(X : Type u_1) → [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → CompHaus

A constructor for objects of the category CompHaus, taking a type, and bundling the compact Hausdorff topology found by typeclass inference.

Defined in

Mathlib.Topology.Category.CompHaus.Basic

Cited by

11 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TopologicalSpaceCompactSpaceT2Space