Loogle!

Result

Found 34 declarations mentioning CategoryTheory.Limits.Pi.map.

• CategoryTheory.Limits.Pi.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) : ∏ᶜ f ⟶ ∏ᶜ g
• CategoryTheory.Limits.Pi.map_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} [CategoryTheory.Limits.HasProduct f] : (CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∏ᶜ f)
• CategoryTheory.Limits.Pi.map_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) [∀ (i : β), CategoryTheory.Mono (p i)] : CategoryTheory.Mono (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Pi.map'_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : α) → f b ⟶ g b) : CategoryTheory.Limits.Pi.map' id p = CategoryTheory.Limits.Pi.map p
• CategoryTheory.Limits.Pi.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Pi.map_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p) (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b)
• CategoryTheory.Limits.Pi.map_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h : α → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
• CategoryTheory.Limits.Pi.map_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (CategoryTheory.CategoryStruct.comp (p b) h)
• CategoryTheory.Limits.Pi.map'_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g h : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (q' : (b : β) → g b ⟶ h b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map' p q) (CategoryTheory.Limits.Pi.map q') = CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q b) (q' b)
• CategoryTheory.Limits.Pi.map_comp_map' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} {h : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : β → α) (q : (a : α) → f a ⟶ g a) (q' : (b : β) → g (p b) ⟶ h b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map q) (CategoryTheory.Limits.Pi.map' p q') = CategoryTheory.Limits.Pi.map' p fun b => CategoryTheory.CategoryStruct.comp (q (p b)) (q' b)
• CategoryTheory.Limits.Pi.map_π_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) {F : C → C → Type uF} {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (∏ᶜ f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map p)) x) = (CategoryTheory.ConcreteCategory.hom (p b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
• CategoryTheory.Limits.piConst_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type wᵒᵖ) : (CategoryTheory.Limits.piConst.map f).app n = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.piFunctor_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : Type wᵒᵖ) : (CategoryTheory.Limits.piFunctor.map f).app T = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.Pi.map_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Epi (p j)] : CategoryTheory.Epi (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Types.pi_map_π_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {β : Type v} [Small.{u, v} β] {f g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : (fun X => X) (∏ᶜ f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map α)) x) = (CategoryTheory.ConcreteCategory.hom (α b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
• CategoryTheory.Limits.Types.pi_map_π_apply' 📋 Mathlib.CategoryTheory.Limits.Types.Products
  {β : Type v} {f g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : (fun X => X) (∏ᶜ f)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π g b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.map α)) x) = (CategoryTheory.ConcreteCategory.hom (α b)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π f b)) x)
• CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1) [W.RespectsIso] (hW : ∀ (X₁ X₂ : J → C) [inst : CategoryTheory.Limits.HasProduct X₁] [inst_1 : CategoryTheory.Limits.HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Pi.map f)) : W.IsStableUnderProductsOfShape J
• CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteProducts C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Discrete α) C} (β : X✝ ⟶ Y✝) (x✝ : (Finset (CategoryTheory.Discrete α))ᵒᵖ) : ((CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).map β).app x✝ = CategoryTheory.Limits.Pi.map fun x => β.app ↑x
• CategoryTheory.Pretriangulated.productTriangle_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₁ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₁
• CategoryTheory.Pretriangulated.productTriangle_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₂ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₂
• CategoryTheory.Pretriangulated.productTriangle_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] {J : Type u_1} (T : J → CategoryTheory.Pretriangulated.Triangle C) [CategoryTheory.Limits.HasProduct fun j => (T j).obj₁] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₂] [CategoryTheory.Limits.HasProduct fun j => (T j).obj₃] [CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁] : (CategoryTheory.Pretriangulated.productTriangle T).mor₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map fun j => (T j).mor₃) (CategoryTheory.inv (CategoryTheory.Limits.piComparison (CategoryTheory.shiftFunctor C 1) fun j => (T j).obj₁))
• CategoryTheory.instHasLiftingPropertyMap 📋 Mathlib.CategoryTheory.LiftingProperties.Limits
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} {A B : J → C} [CategoryTheory.Limits.HasProduct A] [CategoryTheory.Limits.HasProduct B] (f : (j : J) → A j ⟶ B j) {X Y : C} (p : X ⟶ Y) [∀ (j : J), CategoryTheory.HasLiftingProperty p (f j)] : CategoryTheory.HasLiftingProperty p (CategoryTheory.Limits.Pi.map f)
• HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] : HomotopicalAlgebra.Fibration (CategoryTheory.Limits.Pi.map f)
• HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Fibration (f i)] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] [∀ (i : J), HomotopicalAlgebra.WeakEquivalence (f i)] : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.Pi.map f)
• CategoryTheory.Limits.pointwiseProduct_map 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → CategoryTheory.Category.{v₁, u₁} (I i)] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] (F : (i : α) → CategoryTheory.Functor (I i) C) {X✝ Y✝ : (i : α) → I i} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.pointwiseProduct F).map f = CategoryTheory.Limits.Pi.map fun s => (F s).map (f s)
• CategoryTheory.Limits.coconePointwiseProduct_ι_app 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type w} {I : α → Type u₁} [(i : α) → CategoryTheory.Category.{v₁, u₁} (I i)] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] (F : (i : α) → CategoryTheory.Functor (I i) C) [∀ (i : α), CategoryTheory.Limits.HasColimitsOfShape (I i) C] (k : (i : α) → I i) : (CategoryTheory.Limits.coconePointwiseProduct F).ι.app k = CategoryTheory.Limits.Pi.map fun s => CategoryTheory.Limits.colimit.ι (F s) (k s)
• CategoryTheory.Limits.FormalCoproduct.evalOp_map_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (α : X✝ ⟶ Y✝) (f : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ) : ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).map α).app f = CategoryTheory.Limits.Pi.map fun i => α.app (Opposite.op ((Opposite.unop f).obj i))
• CategoryTheory.Limits.FormalCoproduct.powerMap_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.Limits.FormalCoproduct.powerMap f α).φ = fun i => CategoryTheory.Limits.Pi.map fun a => f.φ (i a)
• CategoryTheory.Limits.Pi.map_eq_prod_map 📋 Mathlib.CategoryTheory.Limits.Shapes.PiProd
  {C : Type u_1} {I : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {X Y : I → C} (f : (i : I) → X i ⟶ Y i) (P : I → Prop) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => X ↑i] [CategoryTheory.Limits.HasProduct fun i => Y ↑i] [CategoryTheory.Limits.HasProduct fun i => Y ↑i] [(i : I) → Decidable (P i)] : CategoryTheory.Limits.Pi.map f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.Pi.map fun i => f ↑i) (CategoryTheory.Limits.Pi.map fun i => f ↑i)) ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).inv)
• CategoryTheory.Limits.SequentialProduct.cone_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
  {C : Type u_1} {M N : ℕ → C} [CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n) [CategoryTheory.Limits.HasCountableProducts C] (n : ℕ) : (CategoryTheory.Limits.SequentialProduct.cone f).π.app (Opposite.op n) = CategoryTheory.Limits.Pi.map fun m => if h : m < n then CategoryTheory.eqToHom ⋯ else CategoryTheory.CategoryStruct.comp (f m) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_map_app 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) (j : Cᵒᵖ) : (Φ.skyscraperPresheafFunctor.map f).app j = CategoryTheory.Limits.Pi.map fun x => f
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (n : ℕ) : ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).map f).f n = CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (X : SimplexCategory) : ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).map f).app X = CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op X)).obj i))
• LightCondensed.instEpiLightCondModMapNat 📋 Mathlib.Condensed.Light.Epi
  {R : Type u} [Ring R] {M N : ℕ → LightCondMod R} (f : (n : ℕ) → M n ⟶ N n) [∀ (n : ℕ), CategoryTheory.Epi (f n)] : CategoryTheory.Epi (CategoryTheory.Limits.Pi.map f)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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 88c39f3 serving mathlib revision 9977002