Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.WalkingCospan.right

CategoryTheory.Limits.WalkingCospan

The right point of the walking cospan.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Cited by
182 results in Mathlib
Foundations
Depth 3 from the axioms, rests on 5 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.Limits.pullback.snd · cited by 637pullback.sndCategoryTheory.Limits.PullbackCone.snd · cited by 113PullbackCone.sndCategoryTheory.Limits.pullback.lift_snd · cited by 30pullback.lift_sndCategoryTheory.Limits.WalkingCospan.Hom.inr · cited by 23Hom.inrCategoryTheory.Limits.pullbackSymmetry_hom_comp_fst · cited by 18Limits.pullbackSymmetry_h…CategoryTheory.Limits.diagramIsoCospan · cited by 17Limits.diagramIsoCospanCategoryTheory.Limits.pullbackSymmetry_hom_comp_snd · cited by 13Limits.pullbackSymmetry_h…CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd · cited by 12IsLimit.lift_sndCategoryTheory.IsPullback.isoPullback_hom_snd · cited by 11IsPullback.isoPullback_ho…CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd · cited by 8Limits.pullbackRightPullb…CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd · cited by 7Limits.pullbackRightPullb…CategoryTheory.Limits.pullback.congrHom_inv · cited by 7pullback.congrHom_invCategoryTheory.Limits.weakPullback.snd · cited by 6weakPullback.sndAlgebraicGeometry.pullbackSpecIso_inv_snd · cited by 6AlgebraicGeometry.pullbac…CategoryTheory.Limits.PreservesPullback.iso_hom_snd · cited by 5PreservesPullback.iso_hom…CategoryTheory.Limits.WalkingCospan · cited by 496Limits.WalkingCospanWalkingCospan.rightCITED BYCITES

Cites1

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

Cited by198

Results whose statement or proof uses this declaration.