Loogle!

Result

Found 92 declarations mentioning CategoryTheory.IsFilteredOrEmpty.

• CategoryTheory.IsFilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.IsFiltered.max 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j j' : C) : C
• CategoryTheory.IsFiltered.toIsFilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFiltered C] : CategoryTheory.IsFilteredOrEmpty C
• CategoryTheory.IsFiltered.max₃ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j₁ j₂ j₃ : C) : C
• CategoryTheory.IsFiltered.mk 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [toIsFilteredOrEmpty : CategoryTheory.IsFilteredOrEmpty C] [nonempty : Nonempty C] : CategoryTheory.IsFiltered C
• CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty Cᵒᵖ] : CategoryTheory.IsCofilteredOrEmpty C
• CategoryTheory.isCofilteredOrEmpty_op_of_isFilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] : CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ
• CategoryTheory.isFilteredOrEmpty_of_isCofilteredOrEmpty_op 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ] : CategoryTheory.IsFilteredOrEmpty C
• CategoryTheory.isFilteredOrEmpty_of_semilatticeSup 📋 Mathlib.CategoryTheory.Filtered.Basic
  (α : Type u) [SemilatticeSup α] : CategoryTheory.IsFilteredOrEmpty α
• CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] : CategoryTheory.IsFilteredOrEmpty Cᵒᵖ
• CategoryTheory.isFilteredOrEmpty_of_directed_le 📋 Mathlib.CategoryTheory.Filtered.Basic
  (α : Type u) [Preorder α] [IsDirectedOrder α] : CategoryTheory.IsFilteredOrEmpty α
• CategoryTheory.IsFilteredOrEmpty.of_equivalence 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D) : CategoryTheory.IsFilteredOrEmpty D
• CategoryTheory.instIsFilteredOrEmptyForall 📋 Mathlib.CategoryTheory.Filtered.Basic
  {α : Type w} {I : α → Type u₁} [(i : α) → CategoryTheory.Category.{v₁, u₁} (I i)] [∀ (i : α), CategoryTheory.IsFilteredOrEmpty (I i)] : CategoryTheory.IsFilteredOrEmpty ((i : α) → I i)
• CategoryTheory.instIsFilteredOrEmptyProd 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsFilteredOrEmpty C] [CategoryTheory.IsFilteredOrEmpty D] : CategoryTheory.IsFilteredOrEmpty (C × D)
• CategoryTheory.IsFiltered.leftToMax 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j j' : C) : j ⟶ CategoryTheory.IsFiltered.max j j'
• CategoryTheory.IsFiltered.rightToMax 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j j' : C) : j' ⟶ CategoryTheory.IsFiltered.max j j'
• CategoryTheory.IsFilteredOrEmpty.of_isRightAdjoint 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (R : CategoryTheory.Functor C D) [R.IsRightAdjoint] : CategoryTheory.IsFilteredOrEmpty D
• CategoryTheory.IsFiltered.firstToMax₃ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j₁ j₂ j₃ : C) : j₁ ⟶ CategoryTheory.IsFiltered.max₃ j₁ j₂ j₃
• CategoryTheory.IsFiltered.secondToMax₃ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j₁ j₂ j₃ : C) : j₂ ⟶ CategoryTheory.IsFiltered.max₃ j₁ j₂ j₃
• CategoryTheory.IsFiltered.thirdToMax₃ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] (j₁ j₂ j₃ : C) : j₃ ⟶ CategoryTheory.IsFiltered.max₃ j₁ j₂ j₃
• CategoryTheory.IsFiltered.coeq 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') : C
• CategoryTheory.IsFilteredOrEmpty.of_right_adjoint 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor D C} {R : CategoryTheory.Functor C D} (h : L ⊣ R) : CategoryTheory.IsFilteredOrEmpty D
• CategoryTheory.IsFiltered.coeq₃ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : C
• CategoryTheory.IsFiltered.coeqHom 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') : j' ⟶ CategoryTheory.IsFiltered.coeq f f'
• CategoryTheory.IsFilteredOrEmpty.cocone_objs 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFilteredOrEmpty C] (X Y : C) : ∃ Z x x, True
• CategoryTheory.IsFiltered.coeq₃Hom 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : j₂ ⟶ CategoryTheory.IsFiltered.coeq₃ f g h
• CategoryTheory.IsFilteredOrEmpty.cocone_maps 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFilteredOrEmpty C] ⦃X Y : C⦄ (f g : X ⟶ Y) : ∃ Z h, CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
• CategoryTheory.IsFiltered.coeq_condition 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') : CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeqHom f f') = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.IsFiltered.coeqHom f f')
• CategoryTheory.IsFiltered.wideSpan 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {I : Type u_1} [Finite I] {i : C} {j : I → C} (f : (x : I) → i ⟶ j x) : ∃ k fik g, ∀ (x : I), CategoryTheory.CategoryStruct.comp (f x) (g x) = fik
• CategoryTheory.IsFiltered.span 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {i j j' : C} (f : i ⟶ j) (f' : i ⟶ j') : ∃ k g g', CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
• CategoryTheory.IsFiltered.coeq₃_condition₁ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h)
• CategoryTheory.IsFiltered.coeq₃_condition₂ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)
• CategoryTheory.IsFiltered.coeq₃_condition₃ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)
• CategoryTheory.IsFiltered.crown 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {ι : Type u_1} [Finite ι] (j : ι → C) {k₁ k₂ : C} (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂) : ∃ s α β, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) α = CategoryTheory.CategoryStruct.comp (g i) β
• CategoryTheory.IsFiltered.coeq_condition_assoc 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') {Z : C} (h : CategoryTheory.IsFiltered.coeq f f' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsFiltered.coeqHom f f') h)
• CategoryTheory.IsFilteredOrEmpty.mk 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (cocone_objs : ∀ (X Y : C), ∃ Z x x, True) (cocone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ Z h, CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) : CategoryTheory.IsFilteredOrEmpty C
• CategoryTheory.IsFiltered.bowtie 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ k₁ k₂ : C} (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) : ∃ s α β, CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β
• CategoryTheory.IsFiltered.crown₃ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ j₃ k₁ k₂ : C} (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) (f₃ : j₃ ⟶ k₁) (g₃ : j₃ ⟶ k₂) : ∃ s α β, CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β ∧ CategoryTheory.CategoryStruct.comp f₃ α = CategoryTheory.CategoryStruct.comp g₃ β
• CategoryTheory.IsFiltered.tulip 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ j₃ k₁ k₂ l : C} (f₁ : j₁ ⟶ k₁) (f₂ : j₂ ⟶ k₁) (f₃ : j₂ ⟶ k₂) (f₄ : j₃ ⟶ k₂) (g₁ : j₁ ⟶ l) (g₂ : j₃ ⟶ l) : ∃ s α β γ, CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp f₃ γ ∧ CategoryTheory.CategoryStruct.comp f₄ γ = CategoryTheory.CategoryStruct.comp g₂ β
• CategoryTheory.IsFiltered.crown₄ 📋 Mathlib.CategoryTheory.Filtered.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ j₃ j₄ k₁ k₂ : C} (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂) (f₃ : j₃ ⟶ k₁) (g₃ : j₃ ⟶ k₂) (f₄ : j₄ ⟶ k₁) (g₄ : j₄ ⟶ k₂) : ∃ s α β, CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧ CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β ∧ CategoryTheory.CategoryStruct.comp f₃ α = CategoryTheory.CategoryStruct.comp g₃ β ∧ CategoryTheory.CategoryStruct.comp f₄ α = CategoryTheory.CategoryStruct.comp g₄ β
• CategoryTheory.Limits.Types.FilteredColimit.rel_equiv 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] : Equivalence (CategoryTheory.Limits.Types.FilteredColimit.Rel F)
• CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_colimitTypeRel 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] : CategoryTheory.Limits.Types.FilteredColimit.Rel F = Relation.EqvGen F.ColimitTypeRel
• CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) xi = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) xj ↔ ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
• CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimit₂ 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) (x₁ x₂ : t.pt) : ∃ j x₁' x₂', (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x₁' = x₁ ∧ (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) x₂' = x₂
• CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.colimitCocone F).ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.Types.colimitCocone F).ι.app j)) xj ↔ CategoryTheory.Limits.Types.FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩
• CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i : J} (x y : F.obj i) : (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y ↔ ∃ j f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y
• CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i j : J} {xi : F.obj i} {xj : F.obj j} : (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) xj ↔ ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
• CategoryTheory.Limits.Types.FilteredColimit.isColimitOf' 📋 Mathlib.CategoryTheory.Limits.Types.Filtered
  {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] (t : CategoryTheory.Limits.Cocone F) (hsurj : ∀ (x : t.pt), ∃ i xi, x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi) (hinj : ∀ (i : J) (x y : (fun X => X) (F.obj i)), (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y → ∃ k f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y) : CategoryTheory.Limits.IsColimit t
• CommRingCat.FilteredColimits.instNontrivialCarrierColimitOfIsFilteredOrEmptyOfObj 📋 Mathlib.Algebra.Category.Ring.FilteredColimits
  {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] [∀ (i : J), Nontrivial ↑(F.obj i)] : Nontrivial ↑(CategoryTheory.Limits.colimit F)
• CommRingCat.FilteredColimits.nontrivial 📋 Mathlib.Algebra.Category.Ring.FilteredColimits
  {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [CategoryTheory.IsFilteredOrEmpty J] [∀ (i : J), Nontrivial ↑(F.obj i)] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : Nontrivial ↑c.pt
• CategoryTheory.Limits.Concrete.exists_hom_ι_eq_of_isColimit 📋 Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {J : Type w} [CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)] [CategoryTheory.IsFilteredOrEmpty J] {D : CategoryTheory.Limits.Cocone F} (hD : CategoryTheory.Limits.IsColimit D) (x : CategoryTheory.ToType D.pt) (k : J) : ∃ j x_1 y, (CategoryTheory.ConcreteCategory.hom (D.ι.app j)) y = x
• CategoryTheory.IsFilteredOrEmpty.of_final 📋 Mathlib.CategoryTheory.Limits.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Final] [CategoryTheory.IsFilteredOrEmpty C] : CategoryTheory.IsFilteredOrEmpty D
• CategoryTheory.IsFilteredOrEmpty.isPreconnected 📋 Mathlib.CategoryTheory.Filtered.Connected
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] : CategoryTheory.IsPreconnected C
• CategoryTheory.IsFilteredOrEmpty.isSiftedOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] : CategoryTheory.IsSiftedOrEmpty C
• CategoryTheory.IsFiltered.under 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (c : C) : CategoryTheory.IsFiltered (CategoryTheory.Under c)
• CategoryTheory.Functor.final_diag_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] : (CategoryTheory.Functor.diag C).Final
• CategoryTheory.Under.final_forget 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (c : C) : (CategoryTheory.Under.forget c).Final
• CategoryTheory.Functor.final_iff_isFiltered_structuredArrow 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] : F.Final ↔ ∀ (d : D), CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)
• CategoryTheory.instIsFilteredStructuredArrowProdDiagOfIsFilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (X : C × C) : CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag C))
• CategoryTheory.StructuredArrow.final_proj_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsFilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Final] (Y : D) : (CategoryTheory.StructuredArrow.proj Y T).Final
• CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) : CategoryTheory.IsFilteredOrEmpty C
• CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) : F.Final
• CategoryTheory.Functor.Final.exists_coeq 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s s' : d ⟶ F.obj c) : ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
• CategoryTheory.Functor.Final.exists_coeq_of_locally_small 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type v₁} [CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s s' : d ⟶ F.obj c) : ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
• CategoryTheory.Functor.final_of_exists_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] (h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)) : F.Final
• CategoryTheory.Functor.final_iff_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] : F.Final ↔ (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
• CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists 📋 Mathlib.CategoryTheory.Filtered.Final
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] (d : D) (h₁ : ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)) : CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow d F)
• CategoryTheory.finallySmall_of_small_weakly_terminal_set 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  {J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFilteredOrEmpty J] (s : Set J) [Small.{v, u} ↑s] (hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)) : CategoryTheory.FinallySmall J
• CategoryTheory.finallySmall_iff_exists_small_weakly_terminal_set 📋 Mathlib.CategoryTheory.Limits.FinallySmall
  (J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFilteredOrEmpty J] : CategoryTheory.FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
• CategoryTheory.Limits.colimit_eq_iff 📋 Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget C)] (F : CategoryTheory.Functor J C) [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] {i j : J} {xi : CategoryTheory.ToType (F.obj i)} {xj : CategoryTheory.ToType (F.obj j)} : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i)) xi = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) xj ↔ ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
• CategoryTheory.Limits.IsColimit.eq_iff' 📋 Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget C)] {F : CategoryTheory.Functor J C} [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i : J} (x y : CategoryTheory.ToType (F.obj i)) : (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) y ↔ ∃ j f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) y
• CategoryTheory.Limits.IsColimit.eq_iff 📋 Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget C)] (F : CategoryTheory.Functor J C) [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i j : J} {xi : CategoryTheory.ToType (F.obj i)} {xj : CategoryTheory.ToType (F.obj j)} : (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) xj ↔ ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
• Set.instPreservesColimitsOfShapeFunctorToTypesOfIsFilteredOrEmpty 📋 Mathlib.CategoryTheory.Limits.Set
  {J : Type w} [CategoryTheory.Category.{w', w} J] {X : Type u} [CategoryTheory.IsFilteredOrEmpty J] : CategoryTheory.Limits.PreservesColimitsOfShape J Set.functorToTypes
• SSet.Subcomplex.instPreservesColimitsOfShapeToSSetFunctorOfIsFilteredOrEmpty 📋 Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation
  {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {X : SSet} [CategoryTheory.IsFilteredOrEmpty J] : CategoryTheory.Limits.PreservesColimitsOfShape J SSet.Subcomplex.toSSetFunctor
• CategoryTheory.IsFiltered.filteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.ObjectProperty C
• CategoryTheory.IsFiltered.SmallFilteredIntermediate 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : Type (max u₁ v)
• CategoryTheory.IsFiltered.filteredClosure.base 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} {f : α → C} (x : α) : CategoryTheory.IsFiltered.filteredClosure f (f x)
• CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : Small.{max v w, u} (CategoryTheory.IsFiltered.filteredClosure f).FullSubcategory
• CategoryTheory.IsFiltered.instSmallCategorySmallFilteredIntermediate 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.SmallCategory (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
• CategoryTheory.IsFiltered.instEssentiallySmallFullSubcategoryFilteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.EssentiallySmall.{max v w, v, u} (CategoryTheory.IsFiltered.filteredClosure f).FullSubcategory
• CategoryTheory.IsFiltered.instIsFilteredOrEmptyFullSubcategoryFilteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.IsFilteredOrEmpty (CategoryTheory.IsFiltered.filteredClosure f).FullSubcategory
• CategoryTheory.IsFiltered.SmallFilteredIntermediate.instIsFilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.IsFilteredOrEmpty (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
• CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor D (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
• CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor (CategoryTheory.IsFiltered.SmallFilteredIntermediate F) C
• CategoryTheory.IsFiltered.SmallFilteredIntermediate.instOfNonempty 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) [Nonempty D] : CategoryTheory.IsFiltered (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
• CategoryTheory.IsFiltered.filteredClosure.max 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : CategoryTheory.IsFiltered.filteredClosure f j → CategoryTheory.IsFiltered.filteredClosure f j' → CategoryTheory.IsFiltered.filteredClosure f (CategoryTheory.IsFiltered.max j j')
• CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFaithfulInclusion 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F).Faithful
• CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFullInclusion 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F).Full
• CategoryTheory.IsFiltered.filteredClosure.coeq 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : CategoryTheory.IsFiltered.filteredClosure f j → CategoryTheory.IsFiltered.filteredClosure f j' → ∀ (f✝ f' : j ⟶ j'), CategoryTheory.IsFiltered.filteredClosure f (CategoryTheory.IsFiltered.coeq f✝ f')
• CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoringCompInclusion 📋 Mathlib.CategoryTheory.Filtered.Small
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : (CategoryTheory.IsFiltered.SmallFilteredIntermediate.factoring F).comp (CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion F) ≅ F
• CategoryTheory.instIsFilteredOrEmptyGrothendieckOfαCategoryObjCat 📋 Mathlib.CategoryTheory.Filtered.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) [CategoryTheory.IsFilteredOrEmpty C] [∀ (c : C), CategoryTheory.IsFilteredOrEmpty ↑(F.obj c)] : CategoryTheory.IsFilteredOrEmpty (CategoryTheory.Grothendieck F)
• CategoryTheory.WithInitial.instIsFilteredOfIsFilteredOrEmpty 📋 Mathlib.CategoryTheory.WithTerminal.Lemmas
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsFilteredOrEmpty C] : CategoryTheory.IsFiltered (CategoryTheory.WithInitial 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