Filtering multisets by a predicate #
Main definitions #
Multiset.filter
:filter p s
is the multiset of elements ins
that satisfyp
.Multiset.filterMap
:filterMap f s
is the multiset ofb
s wheresome b ∈ map f s
.
Filter p s
returns the elements in s
(with the same multiplicities)
which satisfy p
, and removes the rest.
Equations
Instances For
@[simp]
@[simp]
theorem
Multiset.filter_congr
{α : Type u_1}
{p q : α → Prop}
[DecidablePred p]
[DecidablePred q]
{s : Multiset α}
:
@[simp]
@[simp]
theorem
Multiset.filter_le_filter
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
{s t : Multiset α}
(h : s ≤ t)
:
theorem
Multiset.monotone_filter_right
{α : Type u_1}
(s : Multiset α)
⦃p q : α → Prop⦄
[DecidablePred p]
[DecidablePred q]
(h : ∀ (b : α), p b → q b)
:
theorem
Multiset.of_mem_filter
{α : Type u_1}
{p : α → Prop}
[DecidablePred p]
{a : α}
{s : Multiset α}
(h : a ∈ filter p s)
:
p a
theorem
Multiset.mem_of_mem_filter
{α : Type u_1}
{p : α → Prop}
[DecidablePred p]
{a : α}
{s : Multiset α}
(h : a ∈ filter p s)
:
theorem
Multiset.mem_filter_of_mem
{α : Type u_1}
{p : α → Prop}
[DecidablePred p]
{a : α}
{l : Multiset α}
(m : a ∈ l)
(h : p a)
:
@[simp]
theorem
Multiset.filter_filter
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(q : α → Prop)
[DecidablePred q]
(s : Multiset α)
:
theorem
Multiset.filter_comm
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(q : α → Prop)
[DecidablePred q]
(s : Multiset α)
:
theorem
Multiset.map_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]
:
Simultaneously filter and map elements of a multiset #
@[simp]
theorem
Multiset.filter_filterMap
{α : Type u_1}
{β : Type v}
(f : α → Option β)
(p : β → Prop)
[DecidablePred p]
(s : Multiset α)
:
countP #
theorem
Multiset.countP_eq_card_filter
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(s : Multiset α)
:
@[simp]
theorem
Multiset.countP_filter
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(q : α → Prop)
[DecidablePred q]
(s : Multiset α)
:
theorem
Multiset.countP_eq_countP_filter_add
{α : Type u_1}
(s : Multiset α)
(p q : α → Prop)
[DecidablePred p]
[DecidablePred q]
:
Multiplicity of an element #
@[simp]
theorem
Multiset.count_filter_of_pos
{α : Type u_1}
[DecidableEq α]
{p : α → Prop}
[DecidablePred p]
{a : α}
{s : Multiset α}
(h : p a)
:
theorem
Multiset.count_filter_of_neg
{α : Type u_1}
[DecidableEq α]
{p : α → Prop}
[DecidablePred p]
{a : α}
{s : Multiset α}
(h : ¬p a)
:
theorem
Multiset.count_filter
{α : Type u_1}
[DecidableEq α]
{p : α → Prop}
[DecidablePred p]
{a : α}
{s : Multiset α}
:
theorem
Multiset.count_map_eq_count
{α : Type u_1}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
(f : α → β)
(s : Multiset α)
(hf : Set.InjOn f {x : α | x ∈ s})
(x : α)
(H : x ∈ s)
:
Multiset.map f
preserves count
if f
is injective on the set of elements contained in
the multiset
theorem
Multiset.count_map_eq_count'
{α : Type u_1}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
(f : α → β)
(s : Multiset α)
(hf : Function.Injective f)
(x : α)
:
Multiset.map f
preserves count
if f
is injective
Subtraction #
@[simp]
theorem
Multiset.filter_sub
{α : Type u_1}
[DecidableEq α]
(p : α → Prop)
[DecidablePred p]
(s t : Multiset α)
:
@[simp]
theorem
Multiset.sub_filter_eq_filter_not
{α : Type u_1}
[DecidableEq α]
(p : α → Prop)
[DecidablePred p]
(s : Multiset α)
:
@[simp]
@[simp]
theorem
Multiset.map_count_True_eq_filter_card
{α : Type u_1}
(s : Multiset α)
(p : α → Prop)
[DecidablePred p]
:
Mapping a multiset through a predicate and counting the True
s yields the cardinality of the set
filtered by the predicate. Note that this uses the notion of a multiset of Prop
s - due to the
decidability requirements of count
, the decidability instance on the LHS is different from the
RHS. In particular, the decidability instance on the left leaks Classical.decEq
.
See here
for more discussion.
theorem
Multiset.Nodup.filter
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
{s : Multiset α}
:
s.Nodup → (Multiset.filter p s).Nodup
theorem
Multiset.Nodup.erase_eq_filter
{α : Type u_1}
[DecidableEq α]
(a : α)
{s : Multiset α}
:
s.Nodup → s.erase a = Multiset.filter (fun (x : α) => x ≠ a) s
theorem
Multiset.Nodup.notMem_erase
{α : Type u_1}
[DecidableEq α]
{a : α}
{s : Multiset α}
(h : s.Nodup)
:
a ∉ s.erase a
@[deprecated Multiset.Nodup.notMem_erase (since := "2025-05-23")]
theorem
Multiset.Nodup.not_mem_erase
{α : Type u_1}
[DecidableEq α]
{a : α}
{s : Multiset α}
(h : s.Nodup)
:
a ∉ s.erase a
Alias of Multiset.Nodup.notMem_erase
.