ext — Mathlib

English

Two multisets are equal if and only if they have the same multiplicities for every element.

Русский

Два мультимножества равны тогда и только тогда, когда для каждого элемента количества повторений совпадает.

LaTeX

$$$ s = t \iff \forall a, \operatorname{count}(a, s) = \operatorname{count}(a, t) $$$

Lean4

theorem ext {s t : Multiset α} : s = t ↔ ∀ a, count a s = count a t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ =>
    Quotient.eq.trans <| by
      simp only [quot_mk_to_coe, coe_count]
      apply perm_iff_count

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