Loogle!

Result

Found 8664 declarations mentioning Equiv. Of these, 30 have a name containing "curry".

• Equiv.curry 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_9) (β : Type u_10) (γ : Sort u_11) : (α × β → γ) ≃ (α → β → γ)
• Equiv.curry_apply 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_9) (β : Type u_10) (γ : Sort u_11) : ⇑(Equiv.curry α β γ) = Function.curry
• Equiv.curry_symm_apply 📋 Mathlib.Logic.Equiv.Prod
  (α : Type u_9) (β : Type u_10) (γ : Sort u_11) : ⇑(Equiv.curry α β γ).symm = Function.uncurry
• Equiv.piCurry 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) : ((x : (i : α) × β i) → γ x.fst x.snd) ≃ ((a : α) → (b : β a) → γ a b)
• Equiv.piCurry_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (x : (i : α) × β i) → γ x.fst x.snd) : (Equiv.piCurry γ) f = Sigma.curry f
• Equiv.piCurry_symm_apply 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (a : α) → (b : β a) → γ a b) : (Equiv.piCurry γ).symm f = Sigma.uncurry f
• DFinsupp.sigmaCurryEquiv 📋 Mathlib.Data.DFinsupp.Sigma
  {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι] : (Π₀ (i : (x : ι) × α x), δ i.fst i.snd) ≃ Π₀ (i : ι) (j : α i), δ i j
• DFinsupp.sigmaCurryLEquiv_apply 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {R : Type u_3} [Semiring R] {α : ι → Type u_7} {M : (i : ι) → α i → Type u_8} [(i : ι) → (j : α i) → AddCommMonoid (M i j)] [(i : ι) → (j : α i) → Module R (M i j)] [DecidableEq ι] (a✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd) : DFinsupp.sigmaCurryLEquiv a✝ = DFinsupp.sigmaCurryEquiv a✝
• DFinsupp.sigmaCurryLEquiv_symm_apply 📋 Mathlib.LinearAlgebra.DFinsupp
  {ι : Type u_1} {R : Type u_3} [Semiring R] {α : ι → Type u_7} {M : (i : ι) → α i → Type u_8} [(i : ι) → (j : α i) → AddCommMonoid (M i j)] [(i : ι) → (j : α i) → Module R (M i j)] [DecidableEq ι] (a✝ : Π₀ (i : ι) (j : α i), M i j) : DFinsupp.sigmaCurryLEquiv.symm a✝ = DFinsupp.sigmaCurryEquiv.symm a✝
• CategoryTheory.MonoidalClosed.curryHomEquiv' 📋 Mathlib.CategoryTheory.Closed.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} [CategoryTheory.Closed X] : (X ⟶ Y) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ (CategoryTheory.ihom X).obj Y)
• CategoryTheory.MonoidalClosed.curryHomEquiv'_apply 📋 Mathlib.CategoryTheory.Closed.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} [CategoryTheory.Closed X] (f : X ⟶ Y) : CategoryTheory.MonoidalClosed.curryHomEquiv' f = CategoryTheory.MonoidalClosed.curry' f
• CategoryTheory.MonoidalClosed.curryHomEquiv'_symm_apply 📋 Mathlib.CategoryTheory.Closed.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} [CategoryTheory.Closed X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ (CategoryTheory.ihom X).obj Y) : CategoryTheory.MonoidalClosed.curryHomEquiv'.symm g = CategoryTheory.MonoidalClosed.uncurry' g
• CategoryTheory.MonoidalClosed.ofEquiv_curry_def 📋 Mathlib.CategoryTheory.Closed.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.MonoidalClosed.curry f = (adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (F.obj Z))) (CategoryTheory.MonoidalClosed.curry ((adj.toEquivalence.symm.toAdjunction.homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) Z) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y) f)))
• CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def 📋 Mathlib.CategoryTheory.Closed.Monoidal
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : Y ⟶ (CategoryTheory.ihom X).obj Z) : CategoryTheory.MonoidalClosed.uncurry f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y) ((adj.toEquivalence.symm.toAdjunction.homEquiv ((F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm (CategoryTheory.MonoidalClosed.uncurry ((adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f)))
• MultilinearMap.curryFinFinset_apply 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun x => M') M₂) (mk : Fin k → M') (ml : Fin l → M') : (((MultilinearMap.curryFinFinset R M₂ M' hk hl) f) mk) ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
• MultilinearMap.curryFinFinset_symm_apply 📋 Mathlib.LinearAlgebra.Multilinear.Curry
  {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)) (m : Fin n → M') : ((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) m = (f fun i => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m ((finSumEquivOfFinset hk hl) (Sum.inr i))
• LinearIsometryEquiv.piLpCurry_apply 📋 Mathlib.Analysis.Normed.Lp.PiLp
  {𝕜 : Type u_1} [Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7) [(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [(i : ι) → (k : κ i) → Module 𝕜 (α i k)] (f : PiLp p fun i => α i.fst i.snd) : (LinearIsometryEquiv.piLpCurry 𝕜 p α) f = (WithLp.equiv p ((i : ι) → WithLp p ((y : κ i) → α i y))).symm fun i => (WithLp.equiv p ((y : κ i) → α i y)).symm (Sigma.curry ((WithLp.equiv p ((x : Sigma κ) → α x.fst x.snd)) f) i)
• LinearIsometryEquiv.piLpCurry_symm_apply 📋 Mathlib.Analysis.Normed.Lp.PiLp
  {𝕜 : Type u_1} [Semiring 𝕜] {ι : Type u_5} {κ : ι → Type u_6} (p : ENNReal) [Fact (1 ≤ p)] [Fintype ι] [(i : ι) → Fintype (κ i)] (α : (i : ι) → κ i → Type u_7) [(i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] [(i : ι) → (k : κ i) → Module 𝕜 (α i k)] (f : PiLp p fun i => PiLp p (α i)) : (LinearIsometryEquiv.piLpCurry 𝕜 p α).symm f = (WithLp.equiv p ((x : Sigma κ) → α x.fst x.snd)).symm (Sigma.uncurry fun i j => f i j)
• ContinuousMultilinearMap.curryFinFinset_apply 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : ContinuousMultilinearMap 𝕜 (fun i => G) G') (mk : Fin k → G) (ml : Fin l → G) : (((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) mk) ml = f fun i => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
• ContinuousMultilinearMap.curryFinFinset_symm_apply 📋 Mathlib.Analysis.NormedSpace.Multilinear.Curry
  {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : ContinuousMultilinearMap 𝕜 (fun i => G) (ContinuousMultilinearMap 𝕜 (fun i => G) G')) (m : Fin n → G) : ((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) m = (f fun i => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m ((finSumEquivOfFinset hk hl) (Sum.inr i))
• Function.OfArity.curryEquiv 📋 Mathlib.Data.Fin.Tuple.Curry
  {α β : Type u} (n : ℕ) : ((Fin n → α) → β) ≃ Function.OfArity α β n
• Function.FromTypes.curryEquiv 📋 Mathlib.Data.Fin.Tuple.Curry
  {n : ℕ} {τ : Type u} (p : Fin n → Type u) : (((i : Fin n) → p i) → τ) ≃ Function.FromTypes p τ
• Function.OfArity.curryEquiv_apply 📋 Mathlib.Data.Fin.Tuple.Curry
  {α β : Type u} (n : ℕ) (a✝ : (Fin n → α) → β) : (Function.OfArity.curryEquiv n) a✝ = Function.FromTypes.curry a✝
• Function.FromTypes.curryEquiv_apply 📋 Mathlib.Data.Fin.Tuple.Curry
  {n : ℕ} {τ : Type u} (p : Fin n → Type u) (a✝ : ((i : Fin n) → p i) → τ) : (Function.FromTypes.curryEquiv p) a✝ = Function.FromTypes.curry a✝
• Function.OfArity.curryEquiv_symm_apply 📋 Mathlib.Data.Fin.Tuple.Curry
  {α β : Type u} (n : ℕ) (f : Function.FromTypes (fun a => α) β) (a✝ : Fin n → α) : (Function.OfArity.curryEquiv n).symm f a✝ = f.uncurry a✝
• Function.FromTypes.curryEquiv_symm_apply 📋 Mathlib.Data.Fin.Tuple.Curry
  {n : ℕ} {τ : Type u} (p : Fin n → Type u) (f : Function.FromTypes p τ) (a✝ : (i : Fin n) → p i) : (Function.FromTypes.curryEquiv p).symm f a✝ = f.uncurry a✝
• Function.OfArity.curry_two_eq_curry 📋 Mathlib.Data.Fin.Tuple.Curry
  {α β : Type u} (f : (Fin 2 → α) → β) : Function.OfArity.curry f = Function.curry (f ∘ ⇑(finTwoArrowEquiv α).symm)
• Function.OfArity.uncurry_two_eq_uncurry 📋 Mathlib.Data.Fin.Tuple.Curry
  {α β : Type u} (f : Function.OfArity α β 2) : f.uncurry = Function.uncurry f ∘ ⇑(finTwoArrowEquiv α)
• Function.FromTypes.uncurry_two_eq_uncurry 📋 Mathlib.Data.Fin.Tuple.Curry
  (p : Fin 2 → Type u) (τ : Type u) (f : Function.FromTypes p τ) : f.uncurry = Function.uncurry f ∘ ⇑(piFinTwoEquiv p)
• Function.FromTypes.curry_two_eq_curry 📋 Mathlib.Data.Fin.Tuple.Curry
  {p : Fin 2 → Type u} {τ : Type u} (f : ((i : Fin 2) → p i) → τ) : Function.FromTypes.curry f = Function.curry (f ∘ ⇑(piFinTwoEquiv p).symm)

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.

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.

This is Loogle revision 07d4605 serving mathlib revision 2e2176e