English
For any n and x and multiset s, replicate n x ∩ s = replicate min(n, count x s) x.
Русский
Пусть n и x заданы; для мультимножества s верно: replicate n x ∩ s = replicate min(n, count x s) x.
LaTeX
$$$ \\mathrm{replicate}(n, x) \\cap s = \\mathrm{replicate}(\\min(n, \\operatorname{count}(x, s)))\\ x $$$
Lean4
@[simp]
theorem replicate_inter (n : ℕ) (x : α) (s : Multiset α) : replicate n x ∩ s = replicate (min n (s.count x)) x :=
by
ext y
rw [count_inter, count_replicate, count_replicate]
by_cases h : x = y
· simp only [h, if_true]
· simp only [h, if_false, Nat.zero_min]