Loogle!

Result

Found 87 declarations mentioning Multiset.filter.

• Multiset.filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset α
• Multiset.filter_true 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) : Multiset.filter (fun x => True) s = s
• Multiset.Nodup.filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Multiset α} : s.Nodup → (Multiset.filter p s).Nodup
• Multiset.filter_subset 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset.filter p s ⊆ s
• Multiset.countP_eq_card_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset.countP p s = (Multiset.filter p s).card
• Multiset.filter_false 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) : Multiset.filter (fun x => False) s = 0
• Multiset.of_mem_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : a ∈ Multiset.filter p s) : p a
• Multiset.count_eq_card_filter_eq 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : Multiset.count a s = (Multiset.filter (fun x => a = x) s).card
• Multiset.filter_eq 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) : Multiset.filter (Eq b) s = Multiset.replicate (Multiset.count b s) b
• Multiset.filter_le 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset.filter p s ≤ s
• Multiset.monotone_filter_left 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] : Monotone (Multiset.filter p)
• Multiset.filterMap_eq_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] : Multiset.filterMap (Option.guard fun b => decide (p b)) = Multiset.filter p
• Multiset.filter_cons_of_neg 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : ¬p a → Multiset.filter p (a ::ₘ s) = Multiset.filter p s
• Multiset.count_filter_of_pos 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : p a) : Multiset.count a (Multiset.filter p s) = Multiset.count a s
• Multiset.filter_coe 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) : Multiset.filter p ↑l = ↑(List.filter (fun b => decide (p b)) l)
• Multiset.filter_eq' 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) : Multiset.filter (fun x => x = b) s = Multiset.replicate (Multiset.count b s) b
• Multiset.filter_eq_self 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : Multiset.filter p s = s ↔ ∀ a ∈ s, p a
• Multiset.mem_of_mem_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : a ∈ Multiset.filter p s) : a ∈ s
• Multiset.count_filter_of_neg 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : ¬p a) : Multiset.count a (Multiset.filter p s) = 0
• Multiset.filter_cons_of_pos 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : p a → Multiset.filter p (a ::ₘ s) = a ::ₘ Multiset.filter p s
• Multiset.filter_zero 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] : Multiset.filter p 0 = 0
• Multiset.mem_filter_of_mem 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {l : Multiset α} (m : a ∈ l) (h : p a) : a ∈ Multiset.filter p l
• Multiset.map_count_True_eq_filter_card 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : Multiset.count True (Multiset.map p s) = (Multiset.filter p s).card
• Multiset.mem_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} : a ∈ Multiset.filter p s ↔ a ∈ s ∧ p a
• Multiset.filter_comm 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : Multiset.filter p (Multiset.filter q s) = Multiset.filter q (Multiset.filter p s)
• Multiset.Nodup.erase_eq_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] (a : α) {s : Multiset α} : s.Nodup → s.erase a = Multiset.filter (fun x => x ≠ a) s
• Multiset.countP_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] : Multiset.countP p (Multiset.map f s) = (Multiset.filter (fun a => p (f a)) s).card
• Multiset.count_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_3} {β : Type u_4} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) : Multiset.count b (Multiset.map f s) = (Multiset.filter (fun a => b = f a) s).card
• Multiset.count_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} : Multiset.count a (Multiset.filter p s) = if p a then Multiset.count a s else 0
• Multiset.filter_eq_nil 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : Multiset.filter p s = 0 ↔ ∀ a ∈ s, ¬p a
• Multiset.filter.congr_simp 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p p✝ : α → Prop) (e_p : p = p✝) {inst✝ : DecidablePred p} [DecidablePred p✝] (s s✝ : Multiset α) (e_s : s = s✝) : Multiset.filter p s = Multiset.filter p✝ s✝
• Multiset.filter_filterMap 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (f : α → Option β) (p : β → Prop) [DecidablePred p] (s : Multiset α) : Multiset.filter p (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.filter (fun b => decide (p b)) (f x)) s
• Multiset.monotone_filter_right 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q] (h : ∀ (b : α), p b → q b) : Multiset.filter p s ≤ Multiset.filter q s
• Multiset.filterMap_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] (f : α → Option β) (s : Multiset α) : Multiset.filterMap f (Multiset.filter p s) = Multiset.filterMap (fun x => if p x then f x else none) s
• Multiset.filter_congr 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Multiset α} : (∀ x ∈ s, p x ↔ q x) → Multiset.filter p s = Multiset.filter q s
• Multiset.filter_singleton 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {a : α} (p : α → Prop) [DecidablePred p] : Multiset.filter p {a} = if p a then {a} else ∅
• Multiset.map_filter_eq_filterMap 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (f : α → β) (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset.map f (Multiset.filter p s) = Multiset.filterMap (fun a => if p a then some (f a) else none) s
• Multiset.filter_add_not 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset.filter p s + Multiset.filter (fun a => ¬p a) s = s
• Multiset.countP_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : Multiset.countP p (Multiset.filter q s) = Multiset.countP (fun a => p a ∧ q a) s
• Multiset.filter_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : Multiset.filter p (Multiset.filter q s) = Multiset.filter (fun a => p a ∧ q a) s
• Multiset.filter_le_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] {s t : Multiset α} (h : s ≤ t) : Multiset.filter p s ≤ Multiset.filter p t
• Multiset.filter_map 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] (f : β → α) (s : Multiset β) : Multiset.filter p (Multiset.map f s) = Multiset.map f (Multiset.filter (p ∘ f) s)
• Multiset.sub_filter_eq_filter_not 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s : Multiset α) : s - Multiset.filter p s = Multiset.filter (fun a => ¬p a) s
• Multiset.countP_eq_countP_filter_add 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] : Multiset.countP p s = Multiset.countP p (Multiset.filter q s) + Multiset.countP p (Multiset.filter (fun a => ¬q a) s)
• Multiset.filter_add 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s t : Multiset α) : Multiset.filter p (s + t) = Multiset.filter p s + Multiset.filter p t
• Multiset.le_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {s t : Multiset α} : s ≤ Multiset.filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a
• Multiset.filter_sub 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) : Multiset.filter p (s - t) = Multiset.filter p s - Multiset.filter p t
• Multiset.card_filter_le_iff 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (P : α → Prop) [DecidablePred P] (n : ℕ) : (Multiset.filter P s).card ≤ n ↔ ∀ s' ≤ s, n < s'.card → ∃ a ∈ s', ¬P a
• Multiset.filter_cons 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : Multiset.filter p (a ::ₘ s) = (if p a then {a} else 0) + Multiset.filter p s
• Multiset.map_filter' 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] {f : α → β} (hf : Function.Injective f) (s : Multiset α) [DecidablePred fun b => ∃ a, p a ∧ f a = b] : Multiset.map f (Multiset.filter p s) = Multiset.filter (fun b => ∃ a, p a ∧ f a = b) (Multiset.map f s)
• Multiset.filter_add_filter 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : Multiset.filter p s + Multiset.filter q s = Multiset.filter (fun a => p a ∨ q a) s + Multiset.filter (fun a => p a ∧ q a) s
• Multiset.filter_attach 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : Multiset.filter (fun a => p ↑a) s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter p s).attach
• Multiset.filter_attach' 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : { a // a ∈ s } → Prop) [DecidableEq α] [DecidablePred p] : Multiset.filter p s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach
• Multiset.filter_inter 📋 Mathlib.Data.Multiset.UnionInter
  {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) : Multiset.filter p (s ∩ t) = Multiset.filter p s ∩ Multiset.filter p t
• Multiset.filter_union 📋 Mathlib.Data.Multiset.UnionInter
  {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) : Multiset.filter p (s ∪ t) = Multiset.filter p s ∪ Multiset.filter p t
• Multiset.ndinter.eq_1 📋 Mathlib.Data.Multiset.FinsetOps
  {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s.ndinter t = Multiset.filter (fun x => x ∈ t) s
• Finset.filter_val 📋 Mathlib.Data.Finset.Filter
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Finset α) : (Finset.filter p s).val = Multiset.filter p s.val
• Multiset.toFinset_filter 📋 Mathlib.Data.Finset.Basic
  {α : Type u_1} [DecidableEq α] (s : Multiset α) (p : α → Prop) [DecidablePred p] : (Multiset.filter p s).toFinset = Finset.filter p s.toFinset
• Multiset.nsmul_count 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Defs
  {M : Type u_3} [AddCommMonoid M] {s : Multiset M} [DecidableEq M] (a : M) : Multiset.count a s • a = (Multiset.filter (Eq a) s).sum
• Multiset.pow_count 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Defs
  {M : Type u_3} [CommMonoid M] {s : Multiset M} [DecidableEq M] (a : M) : a ^ Multiset.count a s = (Multiset.filter (Eq a) s).prod
• Multiset.filter_nsmul 📋 Mathlib.Algebra.Order.Group.Multiset
  {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) (n : ℕ) : Multiset.filter p (n • s) = n • Multiset.filter p s
• Multiset.prod_filter_mul_prod_filter_not 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {M : Type u_5} [CommMonoid M] {s : Multiset M} (p : M → Prop) [DecidablePred p] : (Multiset.filter p s).prod * (Multiset.filter (fun a => ¬p a) s).prod = s.prod
• Multiset.sum_filter_add_sum_filter_not 📋 Mathlib.Algebra.BigOperators.Group.Multiset.Basic
  {M : Type u_5} [AddCommMonoid M] {s : Multiset M} (p : M → Prop) [DecidablePred p] : (Multiset.filter p s).sum + (Multiset.filter (fun a => ¬p a) s).sum = s.sum
• Multiset.filter_join 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} (S : Multiset (Multiset α)) (p : α → Prop) [DecidablePred p] : Multiset.filter p S.join = (Multiset.map (Multiset.filter p) S).join
• Multiset.filter_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (m : Multiset α) (f : α → Multiset β) (p : β → Prop) [DecidablePred p] : Multiset.filter p (m.bind f) = m.bind fun a => Multiset.filter p (f a)
• Multiset.filter_eq_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} (m : Multiset α) (p : α → Prop) [DecidablePred p] : Multiset.filter p m = m.bind fun a => if p a then {a} else 0
• Multiset.bind_filter 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} (m : Multiset α) (p : α → Prop) (f : α → Multiset β) [DecidablePred p] : (Multiset.filter p m).bind f = m.bind fun a => if p a then f a else 0
• Multiset.Ico_filter_le_of_right_le 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b : α} [DecidablePred fun x => b ≤ x] : Multiset.filter (fun x => b ≤ x) (Multiset.Ico a b) = ∅
• Multiset.Ico_filter_lt_of_le_left 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun x => x < c] (hca : c ≤ a) : Multiset.filter (fun x => x < c) (Multiset.Ico a b) = ∅
• Multiset.Ico_filter_le_of_le_left 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun x => c ≤ x] (hca : c ≤ a) : Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico a b
• Multiset.Ico_filter_le_of_left_le 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun x => c ≤ x] (hac : a ≤ c) : Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico c b
• Multiset.Ico_filter_lt_of_le_right 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun x => x < c] (hcb : c ≤ b) : Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a c
• Multiset.Ico_filter_lt_of_right_le 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun x => x < c] (hbc : b ≤ c) : Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a b
• Multiset.Ico_filter_le_left 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidablePred fun x => x ≤ a] (hab : a < b) : Multiset.filter (fun x => x ≤ a) (Multiset.Ico a b) = {a}
• Multiset.Ico_filter_le 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) : Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico (max a c) b
• Multiset.Ico_filter_lt 📋 Mathlib.Order.Interval.Multiset
  {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) : Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a (min b c)
• Sym.filterNe.eq_1 📋 Mathlib.Data.Sym.Basic
  {α : Type u_1} {n : ℕ} [DecidableEq α] (a : α) (m : Sym α n) : Sym.filterNe a m = ⟨⟨Multiset.count a ↑m, ⋯⟩, ⟨Multiset.filter (fun x => a ≠ x) ↑m, ⋯⟩⟩
• Finsupp.supportedEquivFinsupp_apply_support_val 📋 Mathlib.LinearAlgebra.Finsupp.Supported
  {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set α) (a✝ : ↥(Finsupp.supported M R s)) : ((Finsupp.supportedEquivFinsupp s) a✝).support.val = Multiset.map (fun x => ⟨↑x, ⋯⟩) (Multiset.filter (fun x => x ∈ s) (↑a✝).support.val).attach
• Polynomial.filter_roots_map_range_eq_map_roots 📋 Mathlib.Algebra.Polynomial.Roots
  {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {f : A →+* B} [DecidablePred fun x => x ∈ f.range] (hf : Function.Injective ⇑f) (p : Polynomial A) : Multiset.filter (fun x => x ∈ f.range) (Polynomial.map f p).roots = Multiset.map (⇑f) p.roots
• Nat.Partition.ofMultiset_parts 📋 Mathlib.Combinatorics.Enumerative.Partition.Basic
  (l : Multiset ℕ) : (Nat.Partition.ofMultiset l).parts = Multiset.filter (fun x => ¬x = 0) l
• Nat.Partition.ofSums_parts 📋 Mathlib.Combinatorics.Enumerative.Partition.Basic
  (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n) : (Nat.Partition.ofSums n l hl).parts = Multiset.filter (fun x => x ≠ 0) l
• Equiv.Perm.filter_parts_partition_eq_cycleType 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} : Multiset.filter (fun n => 2 ≤ n) σ.partition.parts = σ.cycleType
• Nat.filter_multiset_Ico_card_eq_of_periodic 📋 Mathlib.Data.Nat.Periodic
  (n a : ℕ) (p : ℕ → Prop) [DecidablePred p] (pp : Function.Periodic p a) : (Multiset.filter p (Multiset.Ico n (n + a))).card = Nat.count p a
• BoxIntegral.TaggedPrepartition.filter_boxes_val 📋 Mathlib.Analysis.BoxIntegral.Partition.Tagged
  {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop) : (π.filter p).boxes.val = Multiset.filter (fun J => p J) π.boxes.val
• Multiset.multinomial_filter_ne 📋 Mathlib.Data.Nat.Choose.Multinomial
  {α : Type u_1} [DecidableEq α] (a : α) (m : Multiset α) : m.multinomial = m.card.choose (Multiset.count a m) * (Multiset.filter (fun x => a ≠ x) m).multinomial
• PMF.toOuterMeasure_ofMultiset_apply 📋 Mathlib.Probability.Distributions.Uniform
  {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (t : Set α) : (PMF.ofMultiset s hs).toOuterMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑s.card
• PMF.toMeasure_ofMultiset_apply 📋 Mathlib.Probability.Distributions.Uniform
  {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (t : Set α) [MeasurableSpace α] (ht : MeasurableSet t) : (PMF.ofMultiset s hs).toMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑s.card

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 1c119a3