filter_eq' — Mathlib

English

Let s be a multiset and b an element. The submultiset consisting of all elements of s equal to b is exactly the multiset consisting of b replicated count(b, s) times.

Русский

Пусть s — мультисет, и b — элемент. Подмножество, состоящее из элементов s, равных b, равно мультисету, содержащему b повторённо count(b, s) раз.

LaTeX

$$$ s.filter (x = b) = \\mathrm{replicate}(\\mathrm{count}(b, s), b) $$$

Lean4

theorem filter_eq' (s : Multiset α) (b : α) : s.filter (· = b) = replicate (count b s) b :=
  Quotient.inductionOn s fun l => by
    simp only [quot_mk_to_coe, filter_coe, coe_count]
    rw [List.filter_eq, coe_replicate]

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