Theorems · Definition · category theory

CompHausLike.of

(P : TopCat → Prop) →
  (X : Type u) →
    [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → [CompHausLike.HasProp P X] → CompHausLike P

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

Defined in

Mathlib.Topology.Category.CompHausLike.Basic

Cited by

24 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

TopologicalSpaceCompactSpaceT2SpaceCompHausLike.HasProp