Theorems · Definition · general topology

CompactlyGenerated.ofHom

{X : Type w} →
  [inst : TopologicalSpace X] →
    [inst_1 : UCompactlyGeneratedSpace X] →
      {Y : Type w} →
        [inst_2 : TopologicalSpace Y] →
          [inst_3 : UCompactlyGeneratedSpace Y] → C(X, Y) → (CompactlyGenerated.of X ⟶ CompactlyGenerated.of Y)

Typecheck a ContinuousMap as a morphism in CompactlyGenerated.

Defined in

Mathlib.Topology.Category.CompactlyGenerated

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceUCompactlyGeneratedSpaceTopologicalSpaceUCompactlyGeneratedSpace