replicate_inter — Mathlib

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]

Похожие утверждения