Theorems · Definition · category theory

ContinuousGeneratedByCat.fromGeneratedByTopCat

{ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      CategoryTheory.Functor (GeneratedByTopCat X) (ContinuousGeneratedByCat X)

The functor GeneratedByTopCat X ⥤ ContinuousGeneratedByCat X which is part of the equivalence ContinuousGeneratedByCat.equivalence. It sends an X-generated topological space Y to the topological space Y, considered as an object of ContinuousGeneratedByCat X.

Defined in

Mathlib.Topology.Convenient.Category

Cited by

5 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace