Loogle!
Result
Found 28 declarations mentioning Std.TreeMap.map.
- Std.TreeMap.map 📋 Std.Data.TreeMap.AdditionalOperations
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} (f : α → β → γ) (t : Std.TreeMap α β cmp) : Std.TreeMap α γ cmp - Std.TreeMap.map_id_equiv 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} : (Std.TreeMap.map (fun x v => v) t).Equiv t - Std.TreeMap.keys_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ} : (Std.TreeMap.map f t).keys = t.keys - Std.TreeMap.isEmpty_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} : (Std.TreeMap.map f t).isEmpty = t.isEmpty - Std.TreeMap.size_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} : (Std.TreeMap.map f t).size = t.size - Std.TreeMap.contains_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t).contains k = t.contains k - Std.TreeMap.getKey?_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t).getKey? k = t.getKey? k - Std.TreeMap.filterMap_equiv_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} : (Std.TreeMap.filterMap (fun k v => some (f k v)) t).Equiv (Std.TreeMap.map f t) - Std.TreeMap.getKeyD_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k fallback : α} : (Std.TreeMap.map f t).getKeyD k fallback = t.getKeyD k fallback - Std.TreeMap.contains_of_contains_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t).contains k = true → t.contains k = true - Std.TreeMap.getKey!_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t).getKey! k = t.getKey! k - Std.TreeMap.Equiv.map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} (h : t₁.Equiv t₂) (f : α → β → γ) : (Std.TreeMap.map f t₁).Equiv (Std.TreeMap.map f t₂) - Std.TreeMap.map_map_equiv 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ δ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ} {g : α → γ → δ} : (Std.TreeMap.map g (Std.TreeMap.map f t)).Equiv (Std.TreeMap.map (fun k v => g k (f k v)) t) - Std.TreeMap.mem_of_mem_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} : k ∈ Std.TreeMap.map f t → k ∈ t - Std.TreeMap.mem_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} : k ∈ Std.TreeMap.map f t ↔ k ∈ t - Std.TreeMap.toList_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → γ} : (Std.TreeMap.map f t).toList = List.map (fun p => (p.1, f p.1 p.2)) t.toList - Std.TreeMap.getKey_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.map f t} : (Std.TreeMap.map f t).getKey k h' = t.getKey k ⋯ - Std.TreeMap.getD_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ} : (Std.TreeMap.map f t).getD k fallback = (Option.map (f k) t[k]?).getD fallback - Std.TreeMap.getD_map_of_getKey?_eq_some 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ} (h : t.getKey? k = some k') : (Std.TreeMap.map f t).getD k fallback = (Option.map (f k') t[k]?).getD fallback - Std.TreeMap.getElem?_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t)[k]? = Option.map (f k) t[k]? - Std.TreeMap.getElem!_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Inhabited γ] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t)[k]! = (Option.map (f k) t[k]?).get! - Std.TreeMap.getElem?_map_of_getKey?_eq_some 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k k' : α} (h : t.getKey? k = some k') : (Std.TreeMap.map f t)[k]? = Option.map (f k') t[k]? - Std.TreeMap.getElem!_map_of_getKey?_eq_some 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited γ] {f : α → β → γ} {k k' : α} (h : t.getKey? k = some k') : (Std.TreeMap.map f t)[k]! = (Option.map (f k') t[k]?).get! - Std.TreeMap.getElem_map 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.map f t} : (Std.TreeMap.map f t)[k] = f k t[k] - Std.TreeMap.getElem_map' 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.map f t} : (Std.TreeMap.map f t)[k] = f (t.getKey k ⋯) t[k] - Std.TreeMap.getD_map' 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} {fallback : γ} : (Std.TreeMap.map f t).getD k fallback = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).getD fallback - Std.TreeMap.getElem?_map' 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t)[k]? = Option.pmap (fun v h' => f (t.getKey k h') v) t[k]? ⋯ - Std.TreeMap.getElem!_map' 📋 Std.Data.TreeMap.Lemmas
{α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited γ] {f : α → β → γ} {k : α} : (Std.TreeMap.map f t)[k]! = (Option.pmap (fun v h => f (t.getKey k h) v) t[k]? ⋯).get!
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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.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
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 findtsum_lt_tsum
even though the hypothesisf 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 ee8c038
serving mathlib revision 7a9e177