Loogle!

Result

Found 99 declarations mentioning CategoryTheory.Limits.BinaryFan.

• CategoryTheory.Limits.BinaryFan 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type (max u v)
• CategoryTheory.Limits.BinaryFan.swap 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : CategoryTheory.Limits.BinaryFan Y X
• CategoryTheory.Limits.BinaryCofan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y)
• CategoryTheory.Limits.BinaryCofan.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y)) : CategoryTheory.Limits.BinaryFan X Y
• CategoryTheory.Limits.BinaryFan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryFan X Y) : CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y)
• CategoryTheory.Limits.BinaryFan.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y)) : CategoryTheory.Limits.BinaryCofan X Y
• CategoryTheory.Limits.BinaryFan.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : CategoryTheory.Limits.BinaryFan X Y
• CategoryTheory.Limits.BinaryFan.map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : CategoryTheory.Limits.BinaryFan (F.obj X) (F.obj Y)
• CategoryTheory.Limits.IsLimit.binaryFanSwap 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (I : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsLimit s.swap
• CategoryTheory.Limits.BinaryFan.IsLimit.op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsColimit c.op
• CategoryTheory.Limits.BinaryFan.IsLimit.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y)} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsColimit c.unop
• CategoryTheory.Limits.BinaryFan.assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : CategoryTheory.Limits.BinaryFan X sYZ.pt
• CategoryTheory.Limits.BinaryFan.assocInv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (s : CategoryTheory.Limits.BinaryFan X sYZ.pt) : CategoryTheory.Limits.BinaryFan sXY.pt Z
• CategoryTheory.Limits.BinaryFan.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ s.pt
• CategoryTheory.Limits.BinaryFan.braiding 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} {t : CategoryTheory.Limits.BinaryFan Y X} (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) : s.pt ≅ t.pt
• CategoryTheory.Limits.BinaryFan.fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }
• CategoryTheory.Limits.BinaryFan.snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }
• CategoryTheory.Limits.BinaryCofan.op_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).op = CategoryTheory.Limits.BinaryFan.mk ι₁.op ι₂.op
• CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} : CategoryTheory.Limits.IsLimit (F.mapCone s) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.map F s)
• CategoryTheory.Limits.BinaryFan.leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t) : t.pt ≅ X
• CategoryTheory.Limits.BinaryFan.rightUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : t.pt ≅ X
• CategoryTheory.Limits.isoBinaryFanMk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryFan X Y) : c ≅ CategoryTheory.Limits.BinaryFan.mk c.fst c.snd
• CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal Y) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.fst
• CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsTerminal X) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso c.snd
• CategoryTheory.Limits.BinaryFan.swap_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.swap.fst = s.snd
• CategoryTheory.Limits.BinaryFan.swap_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.swap.snd = s.fst
• CategoryTheory.Limits.BinaryCofan.unop_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : Opposite.op X ⟶ Opposite.op P) (ι₂ : Opposite.op Y ⟶ Opposite.op P) : (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).unop = CategoryTheory.Limits.BinaryFan.mk ι₁.unop ι₂.unop
• CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) s.fst = f
• CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) s.snd = g
• CategoryTheory.Limits.IsLimit.assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} (R : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.assoc Q s)
• CategoryTheory.Limits.IsLimit.binaryFanSwap_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (I : CategoryTheory.Limits.IsLimit s) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair Y X)) : I.binaryFanSwap.lift t = I.lift (CategoryTheory.Limits.BinaryFan.swap t)
• CategoryTheory.Limits.BinaryFan.π_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.π.app { as := CategoryTheory.Limits.WalkingPair.left } = s.fst
• CategoryTheory.Limits.BinaryFan.π_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.π.app { as := CategoryTheory.Limits.WalkingPair.right } = s.snd
• CategoryTheory.Limits.BinaryFan.isLimitFlip 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk c.snd c.fst)
• CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h✝ : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) (CategoryTheory.CategoryStruct.comp s.fst h✝) = CategoryTheory.CategoryStruct.comp f h✝
• CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h✝ : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.IsLimit.lift h f g) (CategoryTheory.CategoryStruct.comp s.snd h✝) = CategoryTheory.CategoryStruct.comp g h✝
• CategoryTheory.Limits.BinaryFan.braiding_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom t.fst = s.snd
• CategoryTheory.Limits.BinaryFan.braiding_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom t.snd = s.fst
• CategoryTheory.Limits.BinaryFan.braiding_inv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv s.fst = t.snd
• CategoryTheory.Limits.BinaryFan.braiding_inv_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv s.snd = t.fst
• CategoryTheory.Limits.BinaryFan.associator 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} (R : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X sYZ.pt} (S : CategoryTheory.Limits.IsLimit t) : s.pt ≅ t.pt
• CategoryTheory.Limits.BinaryFan.leftUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.leftUnitor P Q).hom = t.snd
• CategoryTheory.Limits.BinaryFan.rightUnitor_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).hom = t.fst
• CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y X' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : X ⟶ X') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp c.fst f) c.snd)
• CategoryTheory.Limits.BinaryFan.isLimitCompRightIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Y' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : Y ⟶ Y') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk c.fst (CategoryTheory.CategoryStruct.comp c.snd f))
• CategoryTheory.Limits.BinaryFan.IsLimit.lift' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : { l // CategoryTheory.CategoryStruct.comp l s.fst = f ∧ CategoryTheory.CategoryStruct.comp l s.snd = g }
• CategoryTheory.Limits.BinaryFan.map_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : (CategoryTheory.Limits.BinaryFan.map F s).fst = F.map s.fst
• CategoryTheory.Limits.BinaryFan.map_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : (CategoryTheory.Limits.BinaryFan.map F s).snd = F.map s.snd
• CategoryTheory.Limits.BinaryFan.braiding_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair Y X).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom (CategoryTheory.CategoryStruct.comp t.fst h) = CategoryTheory.CategoryStruct.comp s.snd h
• CategoryTheory.Limits.BinaryFan.braiding_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair Y X).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom (CategoryTheory.CategoryStruct.comp t.snd h) = CategoryTheory.CategoryStruct.comp s.fst h
• CategoryTheory.Limits.BinaryFan.braiding_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv (CategoryTheory.CategoryStruct.comp s.fst h) = CategoryTheory.CategoryStruct.comp t.snd h
• CategoryTheory.Limits.BinaryFan.braiding_inv_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) {Z : C} (h : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv (CategoryTheory.CategoryStruct.comp s.snd h) = CategoryTheory.CategoryStruct.comp t.fst h
• CategoryTheory.Limits.IsLimit.assoc_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} (R : CategoryTheory.Limits.IsLimit s) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X sYZ.pt)) : (P.assoc Q R).lift t = R.lift (CategoryTheory.Limits.BinaryFan.assocInv P t)
• CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g) = h.lift (CategoryTheory.Limits.BinaryFan.mk f g)
• CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) {f g : W ⟶ s.pt} (h₁ : CategoryTheory.CategoryStruct.comp f s.fst = CategoryTheory.CategoryStruct.comp g s.fst) (h₂ : CategoryTheory.CategoryStruct.comp f s.snd = CategoryTheory.CategoryStruct.comp g s.snd) : f = g
• CategoryTheory.Limits.BinaryFan.assocInv_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (s : CategoryTheory.Limits.BinaryFan X sYZ.pt) : (CategoryTheory.Limits.BinaryFan.assocInv P s).snd = CategoryTheory.CategoryStruct.comp s.snd sYZ.snd
• CategoryTheory.Limits.BinaryFan.assoc_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : (CategoryTheory.Limits.BinaryFan.assoc Q s).fst = CategoryTheory.CategoryStruct.comp s.fst sXY.fst
• CategoryTheory.Limits.BinaryFan.isLimitMk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt ⟶ W) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : CategoryTheory.Limits.BinaryFan X Y) (m : s.pt ⟶ W), CategoryTheory.CategoryStruct.comp m fst = s.fst → CategoryTheory.CategoryStruct.comp m snd = s.snd → m = lift s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)
• CategoryTheory.Limits.BinaryFan.assocInv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (P : CategoryTheory.Limits.IsLimit sXY) (s : CategoryTheory.Limits.BinaryFan X sYZ.pt) : (CategoryTheory.Limits.BinaryFan.assocInv P s).fst = CategoryTheory.Limits.BinaryFan.IsLimit.lift P s.fst (CategoryTheory.CategoryStruct.comp s.snd sYZ.fst)
• CategoryTheory.Limits.BinaryFan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryTheory.CategoryStruct.comp e.hom c'.snd) : c ≅ c'
• CategoryTheory.Limits.BinaryFan.assoc_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : (CategoryTheory.Limits.BinaryFan.assoc Q s).snd = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp s.fst sXY.snd) s.snd)
• CategoryTheory.Limits.BinaryFan.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) (lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)) (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.fst = f) (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.snd = g) (uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), CategoryTheory.CategoryStruct.comp m s.fst = f → CategoryTheory.CategoryStruct.comp m s.snd = g → m = lift f g) : CategoryTheory.Limits.IsLimit s
• CategoryTheory.Limits.BinaryFan.rightUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X) (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }))
• CategoryTheory.Limits.BinaryFan.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryTheory.CategoryStruct.comp e.hom c'.snd) : (CategoryTheory.Limits.BinaryFan.ext e h₁ h₂).hom.hom = e.hom
• CategoryTheory.Limits.BinaryFan.leftUnitor_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.leftUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }) (CategoryTheory.CategoryStruct.id { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }.pt))
• CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.IsPullback c.fst c.snd (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
• CategoryTheory.IsPullback.of_is_product 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {c : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit c) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback c.fst c.snd (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
• CommRingCat.prodFan 📋 Mathlib.Algebra.Category.Ring.Constructions
  (A B : CommRingCat) : CategoryTheory.Limits.BinaryFan A B
• CategoryTheory.Limits.Types.binaryProductCone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) : CategoryTheory.Limits.BinaryFan X Y
• CategoryTheory.Limits.Types.binaryProductLimitCone_cone 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone = CategoryTheory.Limits.Types.binaryProductCone X Y
• CategoryTheory.Limits.Types.binaryProductLimit_lift 📋 Mathlib.CategoryTheory.Limits.Types.Products
  (X Y : Type u) (s : CategoryTheory.Limits.BinaryFan X Y) : (CategoryTheory.Limits.Types.binaryProductLimit X Y).lift s = TypeCat.ofHom fun x => ((CategoryTheory.ConcreteCategory.hom s.fst) x, (CategoryTheory.ConcreteCategory.hom s.snd) x)
• CategoryTheory.extendFan 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : CategoryTheory.Limits.Fan f
• CategoryTheory.extendFan_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) : (CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
• CategoryTheory.extendFanIsLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Fan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) : CategoryTheory.Limits.IsLimit (CategoryTheory.extendFan c₁ c₂)
• CategoryTheory.extendFan_π_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendFan c₁ c₂).π.app X = Fin.cases c₂.fst (fun i => CategoryTheory.CategoryStruct.comp c₂.snd (c₁.π.app { as := i })) X.as
• CategoryTheory.ObjectProperty.prop_of_isLimit_binaryFan 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderBinaryProducts] {X Y : C} {B : CategoryTheory.Limits.BinaryFan X Y} (hB : CategoryTheory.Limits.IsLimit B) (hX : P X) (hY : P Y) : P B.pt
• TopCat.prodBinaryFan 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  (X Y : TopCat) : CategoryTheory.Limits.BinaryFan X Y
• Preorder.semilatticeInfOfIsLimitBinaryFan 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [PartialOrder C] (c : (X Y : C) → CategoryTheory.Limits.BinaryFan X Y) (h : (X Y : C) → CategoryTheory.Limits.IsLimit (c X Y)) : SemilatticeInf C
• CategoryTheory.Limits.pullbackConeEquivBinaryFan 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : CategoryTheory.Limits.PullbackCone f g ≌ CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)
• CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c : CategoryTheory.Limits.PullbackCone f g} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.obj c)
• CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanInverse 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.obj c)
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} (c : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.obj c = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Over.homMk c.fst ⋯) (CategoryTheory.Over.homMk c.snd ⋯)
• CategoryTheory.Over.isPullback_of_binaryFan_isLimit 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y Z : CategoryTheory.Over X} (c : CategoryTheory.Limits.BinaryFan Y Z) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsPullback (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) Y.hom Z.hom
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} (c : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)) : CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.obj c = CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) ⋯
• CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanFunctor_lift_left 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c : CategoryTheory.Limits.PullbackCone f g} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)) : (hc.pullbackConeEquivBinaryFanFunctor.lift s).left = hc.lift (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left s.fst) (CategoryTheory.Over.Hom.left s.snd) ⋯)
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c₁ c₂ : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.map a).hom = CategoryTheory.Over.Hom.left a.hom
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} {c₁ c₂ : CategoryTheory.Limits.PullbackCone f g} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pullbackConeEquivBinaryFan.functor.map a).hom = CategoryTheory.Over.homMk a.hom ⋯
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_unitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : CategoryTheory.Limits.pullbackConeEquivBinaryFan.unitIso = CategoryTheory.NatIso.ofComponents (fun c => c.eta) ⋯
• CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X} : CategoryTheory.Limits.pullbackConeEquivBinaryFan.counitIso = CategoryTheory.NatIso.ofComponents (fun X_1 => CategoryTheory.Limits.BinaryFan.ext (CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (({ obj := fun c => CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) ⋯, map := fun {c₁ c₂} a => { hom := CategoryTheory.Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Over.homMk c.fst ⋯) (CategoryTheory.Over.homMk c.snd ⋯), map := fun {c₁ c₂} a => { hom := CategoryTheory.Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj X_1).pt.left) ⋯) ⋯ ⋯) ⋯
• CategoryTheory.Limits.binaryFanZeroLeft 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.BinaryFan 0 X
• CategoryTheory.Limits.binaryFanZeroRight 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.BinaryFan X 0
• CategoryTheory.Cat.prodCone 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
  (C D : CategoryTheory.Cat) : CategoryTheory.Limits.BinaryFan C D
• CategoryTheory.Limits.Fan.combPairHoms 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} (c₁ : CategoryTheory.Limits.Fan f₁) (c₂ : CategoryTheory.Limits.Fan f₂) (bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt) (i : ι₁ ⊕ ι₂) : bc.pt ⟶ Sum.elim f₁ f₂ i
• CategoryTheory.Limits.Fan.combPairIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} {c₁ : CategoryTheory.Limits.Fan f₁} {c₂ : CategoryTheory.Limits.Fan f₂} {bc : CategoryTheory.Limits.BinaryFan c₁.pt c₂.pt} (h₁ : CategoryTheory.Limits.IsLimit c₁) (h₂ : CategoryTheory.Limits.IsLimit c₂) (h : CategoryTheory.Limits.IsLimit bc) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk bc.pt (c₁.combPairHoms c₂ bc))
• CategoryTheory.FunctorToTypes.binaryProductCone 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Limits.BinaryFan F G
• CategoryTheory.FunctorToTypes.binaryProductLimit_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (s : CategoryTheory.Limits.BinaryFan F G) : (CategoryTheory.FunctorToTypes.binaryProductLimit F G).lift s = CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd
• CategoryTheory.Limits.Pi.binaryFanOfProp 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
  {C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] (X : I → C) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => X ↑i] : CategoryTheory.Limits.BinaryFan (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i)
• CategoryTheory.ChosenPullbacksAlong.binaryFan 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (Y Z : CategoryTheory.Over X) [CategoryTheory.ChosenPullbacksAlong Z.hom] : CategoryTheory.Limits.BinaryFan Y Z
• CompHausLike.productCone 📋 Mathlib.Topology.Category.CompHausLike.Cartesian
  {P : TopCat → Prop} (X Y : CompHausLike P) [CompHausLike.HasProp P (↑X.toTop × ↑Y.toTop)] : CategoryTheory.Limits.BinaryFan X Y

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c