Theorems · Definition · category theory

ContinuousGeneratedByCat.equivalenceUnitIso

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

The unit isomorphism of the equivalence ContinuousGeneratedByCat.equivalence.

Defined in: Mathlib.Topology.Convenient.Category
Cited by: 1 results in Mathlib
Foundations: Depth 90 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.

Cites17

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
CategoryTheory.Functor.idstatement · cited by 3,333
TopCatstatement · cited by 1,889
Homeomorph.symmproof · cited by 365
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

Cited by3

Results whose statement or proof uses this declaration.

ContinuousGeneratedByCat.equivalenceproof · cited by 4
GeneratedByTopCat.adjUnitIsoproof · cited by 1
ContinuousGeneratedByCat.equivalence_unitIsostatement · cited by 0