Loogle!

Result

Found 12 declarations mentioning Behrend.map.

• Behrend.map 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n : ℕ} (d : ℕ) : (Fin n → ℕ) →+ ℕ
• Behrend.map_monotone 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n : ℕ} (d : ℕ) : Monotone ⇑(Behrend.map d)
• Behrend.map_injOn 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n d : ℕ} : Set.InjOn ⇑(Behrend.map d) {x | ∀ (i : Fin n), x i < d}
• Behrend.threeAPFree_image_sphere 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n d k : ℕ} : ThreeAPFree ↑(Finset.image (⇑(Behrend.map (2 * d - 1))) (Behrend.sphere n d k))
• Behrend.map_apply 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n : ℕ} (d : ℕ) (a : Fin n → ℕ) : (Behrend.map d) a = ∑ i, a i * d ^ ↑i
• Behrend.map_mod 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n d : ℕ} (a : Fin n.succ → ℕ) : (Behrend.map d) a % d = a 0 % d
• Behrend.map_zero 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  (d : ℕ) (a : Fin 0 → ℕ) : (Behrend.map d) a = 0
• Behrend.map.eq_1 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n : ℕ} (d : ℕ) : Behrend.map d = { toFun := fun a => ∑ i, a i * d ^ ↑i, map_zero' := ⋯, map_add' := ⋯ }
• Behrend.map_le_of_mem_box 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n d : ℕ} {x : Fin n → ℕ} (hx : x ∈ Behrend.box n d) : (Behrend.map (2 * d - 1)) x ≤ ∑ i, (d - 1) * (2 * d - 1) ^ ↑i
• Behrend.map_succ 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n d : ℕ} (a : Fin (n + 1) → ℕ) : (Behrend.map d) a = a 0 + (∑ x, a x.succ * d ^ ↑x) * d
• Behrend.map_eq_iff 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n d : ℕ} {x₁ x₂ : Fin n.succ → ℕ} (hx₁ : ∀ (i : Fin n.succ), x₁ i < d) (hx₂ : ∀ (i : Fin n.succ), x₂ i < d) : (Behrend.map d) x₁ = (Behrend.map d) x₂ ↔ x₁ 0 = x₂ 0 ∧ (Behrend.map d) (x₁ ∘ Fin.succ) = (Behrend.map d) (x₂ ∘ Fin.succ)
• Behrend.map_succ' 📋 Mathlib.Combinatorics.Additive.AP.Three.Behrend
  {n d : ℕ} (a : Fin (n + 1) → ℕ) : (Behrend.map d) a = a 0 + (Behrend.map d) (a ∘ Fin.succ) * d

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 19971e9 serving mathlib revision bce1d65