Loogle!

Result

Found 38 declarations mentioning Finset.sort. Of these, 37 match your pattern(s).

• Finset.sort_range 📋 Mathlib.Data.Finset.Sort
  (n : ℕ) : ((Finset.range n).sort fun a b => a ≤ b) = List.range n
• Finset.sort_nodup 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : (s.sort r).Nodup
• Finset.pairwise_sort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : List.Pairwise r (s.sort r)
• Finset.sort_sorted 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : List.Pairwise r (s.sort r)
• Finset.sort_perm_toList 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : (s.sort r).Perm s.toList
• Finset.length_sort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {s : Finset α} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : (s.sort r).length = s.card
• Finset.sort_empty 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : ∅.sort r = []
• Finset.sort_eq 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : ↑(s.sort r) = s.val
• Finset.sort_toFinset 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] [DecidableEq α] : (s.sort r).toFinset = s
• Finset.sort_singleton 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (a : α) : {a}.sort r = [a]
• Finset.sort_val 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : s.val.sort r = s.sort r
• Finset.sort.eq_1 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : s.sort r = s.val.sort r
• Finset.mem_sort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {s : Finset α} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] {a : α} : a ∈ s.sort r ↔ a ∈ s
• Finset.sort_mk 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {m : Multiset α} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (h : m.Nodup) : { val := m, nodup := h }.sort r = m.sort r
• 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) : l.toFinset.sort r = l ↔ List.Pairwise r l
• Fin.sort_univ 📋 Mathlib.Data.Finset.Sort
  (n : ℕ) : (Finset.univ.sort fun x y => x ≤ y) = List.finRange n
• Finset.sort_cons 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {s : Finset α} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] {a : α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) : (Finset.cons a s h₂).sort r = a :: s.sort r
• Finset.sort_sorted_lt 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) : (s.sort fun a b => a ≤ b).SortedLT
• Finset.sortedLT_sort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) : (s.sort fun a b => a ≤ b).SortedLT
• Finset.sort_insert 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {s : Finset α} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] [DecidableEq α] {a : α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) : (insert a s).sort r = a :: s.sort r
• Finset.sort_sorted_gt 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) : (s.sort fun x1 x2 => x1 ≥ x2).SortedGT
• Finset.sortedGT_sort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) : (s.sort fun x1 x2 => x1 ≥ x2).SortedGT
• Finset.min'_eq_sorted_zero 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] {s : Finset α} {h : s.Nonempty} : s.min' h = (s.sort fun a b => a ≤ b)[0]
• Finset.listMap_orderEmbOfFin_finRange 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) : List.map (⇑(s.orderEmbOfFin h)) (List.finRange k) = s.sort fun a b => a ≤ b
• Finset.map_sort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [IsTotal β r'] (hs : ∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) : List.map (⇑f) (s.sort r) = (Finset.map f s).sort r'
• Finset.sort.congr_simp 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} (s s✝ : Finset α) (e_s : s = s✝) (r r✝ : α → α → Prop) (e_r : r = r✝) {inst✝ : DecidableRel r} [DecidableRel r✝] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] : s.sort r = s✝.sort r✝
• Finset.max'_eq_sorted_last 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] {s : Finset α} {h : s.Nonempty} : s.max' h = (s.sort fun a b => a ≤ b)[(s.sort fun a b => a ≤ b).length - 1]
• Finset.orderEmbOfFin_apply 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : (s.orderEmbOfFin h) i = (s.sort fun a b => a ≤ b)[i]
• Finset.sorted_zero_eq_min' 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] {s : Finset α} {h : 0 < (s.sort fun a b => a ≤ b).length} : (s.sort fun a b => a ≤ b)[0] = s.min' ⋯
• StrictMonoOn.map_finsetSort 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) [LinearOrder α] [LinearOrder β] (hf : StrictMonoOn ⇑f ↑s) : List.map (⇑f) (s.sort fun a b => a ≤ b) = (Finset.map f s).sort fun a b => a ≤ b
• Finset.sorted_zero_eq_min'_aux 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) (h : 0 < (s.sort fun a b => a ≤ b).length) (H : s.Nonempty) : (s.sort fun a b => a ≤ b).get ⟨0, h⟩ = s.min' H
• Finset.sorted_last_eq_max'_aux 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) (h : (s.sort fun a b => a ≤ b).length - 1 < (s.sort fun a b => a ≤ b).length) (H : s.Nonempty) : (s.sort fun a b => a ≤ b)[(s.sort fun a b => a ≤ b).length - 1] = s.max' H
• Finset.sorted_last_eq_max' 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] {s : Finset α} {h : (s.sort fun a b => a ≤ b).length - 1 < (s.sort fun a b => a ≤ b).length} : (s.sort fun a b => a ≤ b)[(s.sort fun a b => a ≤ b).length - 1] = s.max' ⋯
• Finset.orderIsoOfFin_symm_apply 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (x : ↥s) : ↑((s.orderIsoOfFin h).symm x) = List.idxOf (↑x) (s.sort fun a b => a ≤ b)
• Nat.nth_eq_getD_sort 📋 Mathlib.Data.Nat.Nth
  {p : ℕ → Prop} (h : (setOf p).Finite) (n : ℕ) : Nat.nth p n = (h.toFinset.sort fun a b => a ≤ b).getD n 0
• Nat.nth.eq_1 📋 Mathlib.Data.Nat.Nth
  (p : ℕ → Prop) (n : ℕ) : Nat.nth p n = if h : (setOf p).Finite then (h.toFinset.sort fun a b => a ≤ b).getD n 0 else ↑((Nat.Subtype.orderIsoOfNat (setOf p)) n)
• Profinite.NobelingProof.factors.eq_1 📋 Mathlib.Topology.Category.Profinite.Nobeling.Span
  {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)) : Profinite.NobelingProof.factors C s x = List.map (fun i => if ↑x i = true then Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) i else 1 - Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun x => x ∈ s) i) (s.sort fun x1 x2 => x1 ≥ x2)

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 6ff4759 serving mathlib revision 519f454