Theorems · Definition · category theory

ContinuousGeneratedByCat.equivalenceFunctorIso

{ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      ContinuousGeneratedByCat.fromGeneratedByTopCat.comp (ContinuousGeneratedByCat.toTopCat X) ≅
        GeneratedByTopCat.toTopCat

The isomorphism between fromGeneratedByTopCat ⋙ toTopCat X ≅ GeneratedByTopCat.toTopCat.

Defined in: Mathlib.Topology.Convenient.Category
Cited by: 0 results in Mathlib
Foundations: Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
CategoryTheory.Functorstatement · cited by 16,252
CategoryTheory.Functor.compstatement · cited by 6,529
CategoryTheory.Isostatement · cited by 3,963
TopCatstatement · cited by 1,889
CategoryTheory.NatIso.ofComponentsproof · cited by 178
ContinuousGeneratedByCatstatement · cited by 23
TopCat.isoOfHomeoproof · cited by 12
TopCat.generatedBystatement · cited by 11
GeneratedByTopCatstatement and proof · cited by 10
Topology.IsGeneratedBy.homeomorphproof · cited by 6
ContinuousGeneratedByCat.fromGeneratedByTopCatstatement · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.