Theorems · Theorem · category theory

CompHausLike.ofHom_comp

∀ (P : TopCat → Prop) {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X]
  [inst_3 : CompHausLike.HasProp P X] {Y : Type u} [inst_4 : TopologicalSpace Y] [inst_5 : CompactSpace Y]
  [inst_6 : T2Space Y] [inst_7 : CompHausLike.HasProp P Y] {Z : Type u} [inst_8 : TopologicalSpace Z]
  [inst_9 : CompactSpace Z] [inst_10 : T2Space Z] [inst_11 : CompHausLike.HasProp P Z] (f : C(X, Y)) (g : C(Y, Z)),
  CompHausLike.ofHom P (g.comp f) = CategoryTheory.CategoryStruct.comp (CompHausLike.ofHom P f) (CompHausLike.ofHom P g)

Defined in

Mathlib.Topology.Category.CompHausLike.Basic

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceCompactSpaceT2SpaceCompHausLike.HasPropTopologicalSpaceCompactSpaceT2SpaceCompHausLike.HasPropTopologicalSpaceCompactSpaceT2SpaceCompHausLike.HasProp