Theorems · Definition · category theory

CompHausLike.ofHom

(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] → C(X, Y) → (CompHausLike.of P X ⟶ CompHausLike.of P Y)

Typecheck a continuous map as a morphism in the category CompHausLike P.

Defined in

Mathlib.Topology.Category.CompHausLike.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCompactSpaceT2SpaceCompHausLike.HasPropTopologicalSpaceCompactSpaceT2SpaceCompHausLike.HasProp