Loogle!

Result

Found 78 declarations mentioning CategoryTheory.SmallObject.SuccStruct.

• CategoryTheory.SmallObject.SuccStruct 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)
• CategoryTheory.SmallObject.SuccStruct.X₀ 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.SmallObject.SuccStruct C) : C
• CategoryTheory.SmallObject.SuccStruct.succ 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.SmallObject.SuccStruct C) (X : C) : C
• CategoryTheory.SmallObject.SuccStruct.toSuccArrow 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C) : CategoryTheory.Arrow C
• CategoryTheory.SmallObject.SuccStruct.prop 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) : CategoryTheory.MorphismProperty C
• CategoryTheory.SmallObject.SuccStruct.mk 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X₀ : C) (succ : C → C) (toSucc : (X : C) → X ⟶ succ X) : CategoryTheory.SmallObject.SuccStruct C
• CategoryTheory.SmallObject.SuccStruct.toSucc 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.SmallObject.SuccStruct C) (X : C) : X ⟶ self.succ X
• CategoryTheory.SmallObject.SuccStruct.prop_toSucc 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C) : Φ.prop (Φ.toSucc X)
• CategoryTheory.SmallObject.SuccStruct.toSuccArrow_left 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C) : (Φ.toSuccArrow X).left = X
• CategoryTheory.SmallObject.SuccStruct.toSuccArrow_right 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C) : (Φ.toSuccArrow X).right = Φ.succ X
• CategoryTheory.SmallObject.SuccStruct.prop.succ_eq 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : Φ.succ X = Y
• CategoryTheory.SmallObject.SuccStruct.prop_iff 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {X Y : C} (f : X ⟶ Y) : Φ.prop f ↔ CategoryTheory.Arrow.mk f = Φ.toSuccArrow X
• CategoryTheory.SmallObject.SuccStruct.prop.arrowIso 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : CategoryTheory.Arrow.mk f ≅ Φ.toSuccArrow X
• CategoryTheory.SmallObject.SuccStruct.toSuccArrow_hom 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (X : C) : (Φ.toSuccArrow X).hom = Φ.toSucc X
• CategoryTheory.SmallObject.SuccStruct.ofNatTrans 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C ⟶ F) : CategoryTheory.SmallObject.SuccStruct (CategoryTheory.Functor C C)
• CategoryTheory.SmallObject.SuccStruct.Iteration 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} (Φ : CategoryTheory.SmallObject.SuccStruct C) [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] (j : J) : Type (max (max u v) w)
• CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} : Subsingleton (Φ.Iteration j)
• CategoryTheory.SmallObject.SuccStruct.prop.fac 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : f = CategoryTheory.CategoryStruct.comp (Φ.toSucc X) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.SmallObject.SuccStruct.Iteration.trunc 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) {j' : J} (hj' : j' ≤ j) : Φ.Iteration j'
• CategoryTheory.SmallObject.SuccStruct.prop.fac_assoc 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp (Φ.toSucc X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
• CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_hom_left 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : hf.arrowIso.hom.left = CategoryTheory.CategoryStruct.id X
• CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_inv_left 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : hf.arrowIso.inv.left = CategoryTheory.CategoryStruct.id X
• CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_hom_right 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : hf.arrowIso.hom.right = CategoryTheory.eqToHom ⋯
• CategoryTheory.SmallObject.SuccStruct.Iteration.F 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (self : Φ.Iteration j) : CategoryTheory.Functor (↑(Set.Iic j)) C
• CategoryTheory.SmallObject.SuccStruct.prop.arrowIso_inv_right 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {X Y : C} {f : X ⟶ Y} (hf : Φ.prop f) : hf.arrowIso.inv.right = CategoryTheory.eqToHom ⋯
• CategoryTheory.SmallObject.SuccStruct.Iteration.congr_arrowMap 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) : CategoryTheory.SmallObject.SuccStruct.arrowMap iter₁.F k₁ k₂ h h₁ = CategoryTheory.SmallObject.SuccStruct.arrowMap iter₂.F k₁ k₂ h h₂
• CategoryTheory.SmallObject.SuccStruct.Iteration.ext 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} {inst✝¹ : LinearOrder J} {inst✝² : SuccOrder J} {inst✝³ : OrderBot J} {inst✝⁴ : CategoryTheory.Limits.HasIterationOfShape J C} {inst✝⁵ : WellFoundedLT J} {j : J} {x y : Φ.Iteration j} (F : x.F = y.F) : x = y
• CategoryTheory.SmallObject.SuccStruct.Iteration.ext_iff 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} {inst✝¹ : LinearOrder J} {inst✝² : SuccOrder J} {inst✝³ : OrderBot J} {inst✝⁴ : CategoryTheory.Limits.HasIterationOfShape J C} {inst✝⁵ : WellFoundedLT J} {j : J} {x y : Φ.Iteration j} : x = y ↔ x.F = y.F
• CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (self : Φ.Iteration j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i) : CategoryTheory.SmallObject.SuccStruct.arrowMap self.F k i ⋯ hij = CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT self.F hij) hi k hk
• CategoryTheory.SmallObject.SuccStruct.Iteration.trunc_F 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) {j' : J} (hj' : j' ≤ j) : (iter.trunc hj').F = CategoryTheory.SmallObject.restrictionLE iter.F hj'
• CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (self : Φ.Iteration j) : self.F.obj ⟨⊥, ⋯⟩ = Φ.X₀
• CategoryTheory.SmallObject.SuccStruct.Iteration.isColimit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : CategoryTheory.Limits.IsColimit (CategoryTheory.SmallObject.coconeOfLE iter.F hij)
• CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (self : Φ.Iteration j) (i : J) (hi : i < j) : CategoryTheory.SmallObject.SuccStruct.arrowSucc self.F i hi = Φ.toSuccArrow (self.F.obj ⟨i, ⋯⟩)
• CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (k : J) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) : iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩
• CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) (i : J) (hi : i < j) : iter.F.obj ⟨Order.succ i, ⋯⟩ = Φ.succ (iter.F.obj ⟨i, ⋯⟩)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) : iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩
• CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) : CategoryTheory.Arrow.mk (iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj) = CategoryTheory.SmallObject.SuccStruct.arrowMap iter₂.F k₁ k₂ h₁₂ h₂
• CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : iter.F.obj ⟨i, hij⟩ = CategoryTheory.Limits.colimit (CategoryTheory.SmallObject.restrictionLT iter.F hij)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mk 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (obj_bot : F.obj ⟨⊥, ⋯⟩ = Φ.X₀) (arrowSucc_eq : ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩)) (arrowMap_limit : ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i), CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij = CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk) : Φ.Iteration j
• CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_refl 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) {k l : J} (h : k ≤ l) (h' : l ≤ j) : iter.mapObj iter h ⋯ h' ⋯ = iter.F.map (CategoryTheory.homOfLE h)
• CategoryTheory.SmallObject.SuccStruct.Iteration.prop_map_succ 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j : J} (iter : Φ.Iteration j) (i : J) (hi : i < j) : Φ.prop (iter.F.map (CategoryTheory.homOfLE ⋯))
• CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j₁ j₂ j₃ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂) (h₂₃ : k₂ ≤ k₃) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃) : CategoryTheory.CategoryStruct.comp (iter₁.mapObj iter₂ h₁₂ h₁ h₂ h₁₂') (iter₂.mapObj iter₃ h₂₃ h₂ h₃ h₂₃') = iter₁.mapObj iter₃ ⋯ h₁ h₃ ⋯
• CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans_assoc 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j₁ j₂ j₃ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂) (h₂₃ : k₂ ≤ k₃) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃) {Z : C} (h : iter₃.F.obj ⟨k₃, h₃⟩ ⟶ Z) : CategoryTheory.CategoryStruct.comp (iter₁.mapObj iter₂ h₁₂ h₁ h₂ h₁₂') (CategoryTheory.CategoryStruct.comp (iter₂.mapObj iter₃ h₂₃ h₂ h₃ h₂₃') h) = CategoryTheory.CategoryStruct.comp (iter₁.mapObj iter₃ ⋯ h₁ h₃ ⋯) h
• CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C} [LinearOrder J] [SuccOrder J] [OrderBot J] [CategoryTheory.Limits.HasIterationOfShape J C] [WellFoundedLT J] {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) : iter₁.F.map (CategoryTheory.homOfLE h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (iter₂.F.map (CategoryTheory.homOfLE h)) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.SmallObject.SuccStruct.Iteration.nonempty 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (j : J) : Nonempty (Φ.Iteration j)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfBot 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type u) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : Φ.Iteration ⊥
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfSucc 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : ¬IsMax j) (iter : Φ.Iteration j) : Φ.Iteration (Order.succ j)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) : Φ.Iteration j
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i) : CategoryTheory.Functor (↑(Set.Iio j)) C
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) : CategoryTheory.Functor (↑(Set.Iic j)) C
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k) : (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) : CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter) i₁ i₂ h₁₂ ⋯ = CategoryTheory.Arrow.mk ((iter i₁ ⋯).mapObj (iter i₂ h₂) h₁₂ ⋯ ⋯ h₁₂)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_obj 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i) (i : ↑(Set.Iio j)) : (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem iter).obj i = (iter ↑i ⋯).F.obj ⟨↑i, ⋯⟩
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j) : CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor hj iter) i j ⋯ ⋯ = CategoryTheory.Arrow.mk (CategoryTheory.Limits.colimit.ι (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem iter) ⟨i, hi⟩)
• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_map 📋 Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i) {i₁ i₂ : ↑(Set.Iio j)} (f : i₁ ⟶ i₂) : (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem iter).map f = (iter ↑i₁ ⋯).mapObj (iter ↑i₂ ⋯) ⋯ ⋯ ⋯ ⋯
• CategoryTheory.SmallObject.SuccStruct.iteration 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : C
• CategoryTheory.SmallObject.SuccStruct.iter 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (j : J) : Φ.Iteration j
• CategoryTheory.SmallObject.SuccStruct.iterationFunctor 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : CategoryTheory.Functor J C
• CategoryTheory.SmallObject.SuccStruct.ιIteration 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : Φ.X₀ ⟶ Φ.iteration J
• CategoryTheory.SmallObject.SuccStruct.instIsWellOrderContinuousIterationFunctor 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (Φ.iterationFunctor J).IsWellOrderContinuous
• CategoryTheory.SmallObject.SuccStruct.iterationCocone 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : CategoryTheory.Limits.Cocone (Φ.iterationFunctor J)
• CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : Φ.prop.TransfiniteCompositionOfShape J (Φ.ιIteration J)
• CategoryTheory.SmallObject.SuccStruct.isColimitIterationCocone 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : CategoryTheory.Limits.IsColimit (Φ.iterationCocone J)
• CategoryTheory.SmallObject.SuccStruct.iterationCocone_pt 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (Φ.iterationCocone J).pt = Φ.iteration J
• CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjBotIso 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (Φ.iterationFunctor J).obj ⊥ ≅ Φ.X₀
• CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjSuccIso 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) : (Φ.iterationFunctor J).obj (Order.succ j) ≅ Φ.succ ((Φ.iterationFunctor J).obj j)
• CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_F 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).F = Φ.iterationFunctor J
• CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isColimit 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).isColimit = Φ.isColimitIterationCocone J
• CategoryTheory.SmallObject.SuccStruct.ιIterationFunctor 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (CategoryTheory.Functor.const J).obj Φ.X₀ ⟶ Φ.iterationFunctor J
• CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_isoBot 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).isoBot = Φ.iterationFunctorObjBotIso J
• CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (i : J) {j : J} (iter : Φ.Iteration j) (hi : i ≤ j) : (Φ.iterationFunctor J).obj i = iter.F.obj ⟨i, hi⟩
• CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) : Φ.prop ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯))
• CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_incl 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] : (Φ.transfiniteCompositionOfShapeιIteration J).incl = (Φ.iterationCocone J).ι
• CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) : (Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯) = CategoryTheory.CategoryStruct.comp (Φ.toSucc ((Φ.iterationFunctor J).obj j)) (Φ.iterationFunctorObjSuccIso j hj).inv
• CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ_assoc 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (j : J) (hj : ¬IsMax j) {Z : C} (h : (Φ.iterationFunctor J).obj (Order.succ j) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯)) h = CategoryTheory.CategoryStruct.comp (Φ.toSucc ((Φ.iterationFunctor J).obj j)) (CategoryTheory.CategoryStruct.comp (Φ.iterationFunctorObjSuccIso j hj).inv h)
• CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map 📋 Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
  {C : Type u} [CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [CategoryTheory.Limits.HasIterationOfShape J C] (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) {j : J} (iter : Φ.Iteration j) (hj : i₂ ≤ j) : CategoryTheory.Arrow.mk ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE h₁₂)) = CategoryTheory.Arrow.mk (iter.F.map (CategoryTheory.homOfLE h₁₂))
• CategoryTheory.SmallObject.succStruct 📋 Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
  {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ] : CategoryTheory.SmallObject.SuccStruct (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C))
• CategoryTheory.OrthogonalReflection.succStruct 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (Z₀ : C) : CategoryTheory.SmallObject.SuccStruct C

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