inter_replicate — Mathlib

English

For multisets s and replicate n x, s ∩ replicate n x = replicate min(count x s, n) x.

Русский

Для мультимножеств s и replicate n x верно: s ∩ replicate n x = replicate min(count x s, n) x.

LaTeX

$$$ s \\cap \\mathrm{replicate}(n, x) = \\mathrm{replicate}(\\min(\\operatorname{count}(x, s), n))\\ x $$$

Lean4

@[simp]
theorem inter_replicate (s : Multiset α) (n : ℕ) (x : α) : s ∩ replicate n x = replicate (min (s.count x) n) x := by
  rw [inter_comm, replicate_inter, min_comm]

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