Loogle!

Result

Found 18 declarations mentioning List.toFinset and List.Nodup.

• List.toFinset_toList 📋 Mathlib.Data.Finset.Dedup
  {α : Type u_1} [DecidableEq α] {s : List α} (hs : s.Nodup) : s.toFinset.toList.Perm s
• List.toFinset_eq 📋 Mathlib.Data.Finset.Dedup
  {α : Type u_1} [DecidableEq α] {l : List α} (n : l.Nodup) : { val := ↑l, nodup := n } = l.toFinset
• Finset.exists_list_nodup_eq 📋 Mathlib.Data.Finset.Dedup
  {α : Type u_1} [DecidableEq α] (s : Finset α) : ∃ l, l.Nodup ∧ l.toFinset = s
• List.toFinset_surj_on 📋 Mathlib.Data.Finset.Dedup
  {α : Type u_1} [DecidableEq α] : Set.SurjOn List.toFinset {l | l.Nodup} Set.univ
• List.perm_of_nodup_nodup_toFinset_eq 📋 Mathlib.Data.Finset.Dedup
  {α : Type u_1} [DecidableEq α] {l l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) (h : l.toFinset = l'.toFinset) : l.Perm l'
• List.toFinset_card_of_nodup 📋 Mathlib.Data.Finset.Card
  {α : Type u_1} [DecidableEq α] {l : List α} (h : l.Nodup) : l.toFinset.card = l.length
• List.prod_toFinset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {M : Type u_5} [DecidableEq ι] [CommMonoid M] (f : ι → M) {l : List ι} (_hl : l.Nodup) : l.toFinset.prod f = (List.map f l).prod
• List.sum_toFinset 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {M : Type u_5} [DecidableEq ι] [AddCommMonoid M] (f : ι → M) {l : List ι} (_hl : l.Nodup) : l.toFinset.sum f = (List.map f l).sum
• Finset.noncommProd_toFinset 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (l : List α) (f : α → β) (comm : (↑l.toFinset).Pairwise (Function.onFun Commute f)) (hl : l.Nodup) : l.toFinset.noncommProd f comm = (List.map f l).prod
• Finset.noncommSum_toFinset 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] (l : List α) (f : α → β) (comm : (↑l.toFinset).Pairwise (Function.onFun AddCommute f)) (hl : l.Nodup) : l.toFinset.noncommSum f comm = (List.map f l).sum
• List.pairwise_of_coe_toFinset_pairwise 📋 Mathlib.Data.Finset.Pairwise
  {α : Type u_1} [DecidableEq α] {r : α → α → Prop} {l : List α} (hl : (↑l.toFinset).Pairwise r) (hn : l.Nodup) : List.Pairwise r l
• List.pairwise_iff_coe_toFinset_pairwise 📋 Mathlib.Data.Finset.Pairwise
  {α : Type u_1} [DecidableEq α] {r : α → α → Prop} {l : List α} (hn : l.Nodup) (hs : Symmetric r) : (↑l.toFinset).Pairwise r ↔ List.Pairwise r l
• List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint 📋 Mathlib.Data.Finset.Pairwise
  {α : Type u_5} {ι : Type u_6} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α} (hl : (↑l.toFinset).PairwiseDisjoint f) (hn : l.Nodup) : List.Pairwise (Function.onFun Disjoint f) l
• List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint 📋 Mathlib.Data.Finset.Pairwise
  {α : Type u_5} {ι : Type u_6} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α} (hn : l.Nodup) : (↑l.toFinset).PairwiseDisjoint f ↔ List.Pairwise (Function.onFun Disjoint f) l
• List.toFinset_sort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] [DecidableEq α] {l : List α} (hl : l.Nodup) : Finset.sort r l.toFinset = l ↔ List.Sorted r l
• List.support_formPerm_of_nodup 📋 Mathlib.GroupTheory.Perm.List
  {α : Type u_1} [DecidableEq α] [Fintype α] (l : List α) (h : l.Nodup) (h' : ∀ (x : α), l ≠ [x]) : l.formPerm.support = l.toFinset
• List.support_formPerm_of_nodup' 📋 Mathlib.GroupTheory.Perm.List
  {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (h' : ∀ (x : α), l ≠ [x]) : {x | l.formPerm x ≠ x} = ↑l.toFinset
• Equiv.Perm.cycleFactorsFinset_eq_list_toFinset 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
  {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {l : List (Equiv.Perm α)} (hn : l.Nodup) : σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint l ∧ l.prod = σ

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 3e2b26a