Commit 2023-05-12 18:40 fb165b62

View on Github →

feat: port Topology.Category.Top.Limits.Pullbacks (#3802)

Estimated changes

Modified Mathlib.lean

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

added def TopCat.binaryCofanIsColimit

added theorem TopCat.binaryCofan_isColimit_iff

modified theorem TopCat.embedding_prod_map

modified theorem TopCat.inducing_prod_map

modified theorem TopCat.prod_topology

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

added theorem TopCat.coequalizer_isOpen_iff

added theorem TopCat.coinduced_of_isColimit

added theorem TopCat.colimit_isOpen_iff

added theorem TopCat.colimit_topology

added theorem TopCat.embedding_of_pullback_embeddings

added theorem TopCat.embedding_pullback_to_prod

added theorem TopCat.fst_embedding_of_right_embedding

added theorem TopCat.fst_iso_of_right_embedding_range_subset

added theorem TopCat.fst_openEmbedding_of_right_openEmbedding

added theorem TopCat.inducing_pullback_to_prod

added theorem TopCat.openEmbedding_of_pullback_open_embeddings

added def TopCat.pullbackCone

added def TopCat.pullbackConeIsLimit

added def TopCat.pullbackIsoProdSubtype

added theorem TopCat.pullbackIsoProdSubtype_hom_apply

added theorem TopCat.pullbackIsoProdSubtype_hom_fst

added theorem TopCat.pullbackIsoProdSubtype_hom_snd

added theorem TopCat.pullbackIsoProdSubtype_inv_fst

added theorem TopCat.pullbackIsoProdSubtype_inv_fst_apply

added theorem TopCat.pullbackIsoProdSubtype_inv_snd

added theorem TopCat.pullbackIsoProdSubtype_inv_snd_apply

added theorem TopCat.pullback_fst_image_snd_preimage

added theorem TopCat.pullback_fst_range

added theorem TopCat.pullback_map_embedding_of_embeddings

added theorem TopCat.pullback_map_openEmbedding_of_open_embeddings

added theorem TopCat.pullback_snd_image_fst_preimage

added theorem TopCat.pullback_snd_range

added theorem TopCat.pullback_topology

added theorem TopCat.range_pullback_map

added theorem TopCat.range_pullback_to_prod

added theorem TopCat.snd_embedding_of_left_embedding

added theorem TopCat.snd_iso_of_left_embedding_range_subset

added theorem TopCat.snd_openEmbedding_of_left_openEmbedding