Pullbacks

📁 Source: Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

Statistics

Metric	Count
Definitions pullbackCone, pullbackConeIsLimit, pullbackFst, pullbackHomeoPreimage, pullbackIsoProdSubtype, pullbackSnd	6
Theorems coequalizer_isOpen_iff, fst_isEmbedding_of_right, fst_isOpenEmbedding_of_right, fst_iso_of_right_embedding_range_subset, isEmbedding_of_pullback, isEmbedding_pullback_to_prod, isInducing_pullback_to_prod, isOpenEmbedding_of_pullback, isOpen_iff_of_isColimit_cofork, isQuotientMap_of_isColimit_cofork, pullbackFst_apply, pullbackIsoProdSubtype_hom_apply, pullbackIsoProdSubtype_hom_fst, pullbackIsoProdSubtype_hom_snd, pullbackIsoProdSubtype_inv_fst, pullbackIsoProdSubtype_inv_fst_apply, pullbackIsoProdSubtype_inv_fst_assoc, pullbackIsoProdSubtype_inv_snd, pullbackIsoProdSubtype_inv_snd_apply, pullbackIsoProdSubtype_inv_snd_assoc, pullbackSnd_apply, pullback_fst_image_snd_preimage, pullback_fst_range, pullback_map_isEmbedding, pullback_map_isOpenEmbedding, pullback_snd_image_fst_preimage, pullback_snd_range, pullback_topology, range_pullback_map, range_pullback_to_prod, snd_isEmbedding_of_left, snd_isOpenEmbedding_of_left, snd_iso_of_left_embedding_range_subset	33
Total	39

TopCat

Definitions

Name	Category	Theorems
pullbackCone 📖	CompOp	—
pullbackConeIsLimit 📖	CompOp	—
pullbackFst 📖	CompOp	4 math math: pullbackIsoProdSubtype_hom_fst, pullbackFst_apply, pullbackIsoProdSubtype_inv_fst_assoc, pullbackIsoProdSubtype_inv_fst
pullbackHomeoPreimage 📖	CompOp	—
pullbackIsoProdSubtype 📖	CompOp	9 math math: pullbackIsoProdSubtype_hom_fst, pullbackIsoProdSubtype_inv_fst_assoc, pullbackIsoProdSubtype_inv_snd_apply, pullbackIsoProdSubtype_inv_fst, pullbackIsoProdSubtype_hom_snd, pullbackIsoProdSubtype_inv_snd, pullbackIsoProdSubtype_inv_fst_apply, pullbackIsoProdSubtype_hom_apply, pullbackIsoProdSubtype_inv_snd_assoc
pullbackSnd 📖	CompOp	4 math math: pullbackSnd_apply, pullbackIsoProdSubtype_hom_snd, pullbackIsoProdSubtype_inv_snd, pullbackIsoProdSubtype_inv_snd_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coequalizer_isOpen_iff 📖	mathematical	—	IsOpen carrier CategoryTheory.Limits.coequalizer TopCat instCategory CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory topCat_hasColimitsOfShape UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.parallelPair str Set.preimage DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.coequalizer.π	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape topCat_hasColimitsOfShape UnivLE.small univLE_of_max UnivLE.self isOpen_iff_of_isColimit_cofork CategoryTheory.Limits.coequalizer.condition
fst_isEmbedding_of_right 📖	mathematical	Topology.IsEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.pullback_fst_iso_of_right_iso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Limits.limit.lift_π Topology.IsEmbedding.comp Homeomorph.isEmbedding pullback_map_isEmbedding
fst_isOpenEmbedding_of_right 📖	mathematical	Topology.IsOpenEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.pullback_fst_iso_of_right_iso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Limits.limit.lift_π Topology.IsOpenEmbedding.comp Homeomorph.isOpenEmbedding pullback_map_isOpenEmbedding CategoryTheory.instMonoId
fst_iso_of_right_embedding_range_subset 📖	mathematical	Topology.IsEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier Set Set.instHasSubset Set.range	CategoryTheory.IsIso CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits fst_isEmbedding_of_right pullback_fst_range Set.mem_range_self continuous_subtype_val continuous_id' CategoryTheory.Iso.isIso_hom
isEmbedding_of_pullback 📖	mathematical	Topology.IsEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits coe_comp CategoryTheory.Limits.limit.w Topology.IsEmbedding.comp snd_isEmbedding_of_left
isEmbedding_pullback_to_prod 📖	mathematical	—	Topology.IsEmbedding carrier CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.prod CategoryTheory.Discrete CategoryTheory.discreteCategory topCat_hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.pair str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits topCat_hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self isInducing_pullback_to_prod mono_iff_injective CategoryTheory.Limits.mono_pullback_to_prod
isInducing_pullback_to_prod 📖	mathematical	—	Topology.IsInducing carrier CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.prod CategoryTheory.Discrete CategoryTheory.discreteCategory topCat_hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.pair str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits topCat_hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self pullback_topology prod_topology induced_inf induced_compose CategoryTheory.Limits.limit.lift_π
isOpenEmbedding_of_pullback 📖	mathematical	Topology.IsOpenEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	CategoryTheory.Limits.limit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingCospan.one CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits coe_comp CategoryTheory.Limits.limit.w Topology.IsOpenEmbedding.comp snd_isOpenEmbedding_of_left
isOpen_iff_of_isColimit_cofork 📖	mathematical	—	IsOpen carrier CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat instCategory CategoryTheory.Limits.parallelPair str CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair.one Set.preimage CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.Cofork.π	—	isOpen_iff_of_isColimit CategoryTheory.Limits.Cocone.w Continuous.isOpen_preimage ContinuousMap.continuous
isQuotientMap_of_isColimit_cofork 📖	mathematical	—	Topology.IsQuotientMap carrier CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory TopCat instCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.Cofork.π	—	Topology.isQuotientMap_iff CategoryTheory.Limits.epi_of_isColimit_cofork isOpen_iff_of_isColimit_cofork
pullbackFst_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd pullbackFst	—	—
pullbackIsoProdSubtype_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan of carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Iso.hom pullbackIsoProdSubtype CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits
pullbackIsoProdSubtype_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan of carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Iso.hom pullbackIsoProdSubtype pullbackFst CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Iso.eq_inv_comp pullbackIsoProdSubtype_inv_fst
pullbackIsoProdSubtype_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan of carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Iso.hom pullbackIsoProdSubtype pullbackSnd CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Iso.eq_inv_comp pullbackIsoProdSubtype_inv_snd
pullbackIsoProdSubtype_inv_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory of carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Iso.inv pullbackIsoProdSubtype CategoryTheory.Limits.pullback.fst pullbackFst	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp
pullbackIsoProdSubtype_inv_fst_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.fst of instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Iso.inv pullbackIsoProdSubtype	—	CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits pullbackIsoProdSubtype_inv_fst
pullbackIsoProdSubtype_inv_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory of carrier DFunLike.coe ContinuousMap str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Iso.inv pullbackIsoProdSubtype CategoryTheory.Limits.pullback.fst pullbackFst	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoProdSubtype_inv_fst
pullbackIsoProdSubtype_inv_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory of carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Iso.inv pullbackIsoProdSubtype CategoryTheory.Limits.pullback.snd pullbackSnd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp
pullbackIsoProdSubtype_inv_snd_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.snd of instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Iso.inv pullbackIsoProdSubtype	—	CategoryTheory.ConcreteCategory.congr_hom CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits pullbackIsoProdSubtype_inv_snd
pullbackIsoProdSubtype_inv_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory of carrier DFunLike.coe ContinuousMap str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Iso.inv pullbackIsoProdSubtype CategoryTheory.Limits.pullback.snd pullbackSnd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackIsoProdSubtype_inv_snd
pullbackSnd_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier instTopologicalSpaceSubtype instTopologicalSpaceProd pullbackSnd	—	—
pullback_fst_image_snd_preimage 📖	mathematical	—	Set.image carrier CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.fst Set.preimage CategoryTheory.Limits.pullback.snd	—	Set.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.congr_fun CategoryTheory.Limits.pullback.condition pullbackIsoProdSubtype_inv_snd_apply pullbackIsoProdSubtype_inv_fst_apply
pullback_fst_range 📖	mathematical	—	Set.range carrier CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.fst setOf	—	Set.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.congr_fun CategoryTheory.Limits.pullback.condition pullbackIsoProdSubtype_inv_fst_apply
pullback_map_isEmbedding 📖	mathematical	Topology.IsEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.map	—	Topology.IsEmbedding.of_comp CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits topCat_hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.self ContinuousMap.continuous_toFun coe_comp Topology.IsEmbedding.comp isEmbedding_prodMap isEmbedding_pullback_to_prod CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.prod.lift_map
pullback_map_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.map	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits pullback_map_isEmbedding Topology.IsOpenEmbedding.isEmbedding range_pullback_map IsOpen.inter Continuous.isOpen_preimage ContinuousMap.continuous_toFun Topology.IsOpenEmbedding.isOpen_range
pullback_snd_image_fst_preimage 📖	mathematical	—	Set.image carrier CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.snd Set.preimage CategoryTheory.Limits.pullback.fst	—	Set.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.congr_fun CategoryTheory.Limits.pullback.condition pullbackIsoProdSubtype_inv_fst_apply pullbackIsoProdSubtype_inv_snd_apply
pullback_snd_range 📖	mathematical	—	Set.range carrier CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.snd setOf	—	Set.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.congr_fun CategoryTheory.Limits.pullback.condition pullbackIsoProdSubtype_inv_snd_apply
pullback_topology 📖	mathematical	—	str CategoryTheory.Limits.pullback TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan TopologicalSpace carrier SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice TopologicalSpace.induced DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits Topology.IsInducing.eq_induced Homeomorph.isInducing induced_inf induced_compose
range_pullback_map 📖	mathematical	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory	Set.range carrier CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.pullback.map Set Set.instInter Set.preimage CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	Set.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.limit.lift_π mono_iff_injective CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.Concrete.limit_ext CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint instIsRightAdjointForgetContinuousMapCarrier CategoryTheory.Limits.limit.w CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Category.assoc pullbackIsoProdSubtype_inv_fst_assoc pullbackIsoProdSubtype_inv_snd_assoc
range_pullback_to_prod 📖	mathematical	—	Set.range carrier CategoryTheory.Limits.prod TopCat instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory topCat_hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.zero CategoryTheory.Limits.pair CategoryTheory.Limits.pullback CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd setOf CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd	—	Set.ext CategoryTheory.Limits.hasLimitOfHasLimitsOfShape topCat_hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small univLE_of_max UnivLE.zero CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.Concrete.limit_ext CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint instIsRightAdjointForgetContinuousMapCarrier CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Limits.limit.lift_π pullbackIsoProdSubtype_inv_fst pullbackIsoProdSubtype_inv_snd
snd_isEmbedding_of_left 📖	mathematical	Topology.IsEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.limit.lift_π Topology.IsEmbedding.comp Homeomorph.isEmbedding pullback_map_isEmbedding
snd_isOpenEmbedding_of_left 📖	mathematical	Topology.IsOpenEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.limit.lift_π Topology.IsOpenEmbedding.comp Homeomorph.isOpenEmbedding pullback_map_isOpenEmbedding CategoryTheory.instMonoId
snd_iso_of_left_embedding_range_subset 📖	mathematical	Topology.IsEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier Set Set.instHasSubset Set.range	CategoryTheory.IsIso CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits snd_isEmbedding_of_left pullback_snd_range Set.mem_range_self continuous_subtype_val continuous_id' CategoryTheory.Iso.isIso_hom

---

← Back to Index