Commit 2023-05-10 06:33 c2a84a85

View on Github →

feat: port Topology.Category.Top.Limits.Products (#3709)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Category/Top/Basic.lean

Modified Mathlib/Topology/Category/Top/Limits/Basic.lean

Created Mathlib/Topology/Category/Top/Limits/Products.lean

added theorem TopCat.embedding_prod_map

added theorem TopCat.induced_of_isLimit

added theorem TopCat.inducing_prod_map

added theorem TopCat.limit_topology

added def TopCat.piFan

added def TopCat.piFanIsLimit

added def TopCat.piIsoPi

added theorem TopCat.piIsoPi_hom_apply

added theorem TopCat.piIsoPi_inv_π

added theorem TopCat.piIsoPi_inv_π_apply

added def TopCat.prodBinaryFan

added def TopCat.prodBinaryFanIsLimit

added def TopCat.prodIsoProd

added theorem TopCat.prodIsoProd_hom_apply

added theorem TopCat.prodIsoProd_hom_fst

added theorem TopCat.prodIsoProd_hom_snd

added theorem TopCat.prodIsoProd_inv_fst

added theorem TopCat.prodIsoProd_inv_snd

added theorem TopCat.prod_topology

added theorem TopCat.range_prod_map

added def TopCat.sigmaCofan

added def TopCat.sigmaCofanIsColimit

added def TopCat.sigmaIsoSigma

added theorem TopCat.sigmaIsoSigma_hom_ι

added theorem TopCat.sigmaIsoSigma_hom_ι_apply

added theorem TopCat.sigmaIsoSigma_inv_apply