ext — Mathlib

English

Two nodup multisets are equal iff they have the same membership for every element.

Русский

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

LaTeX

$$$\\forall s,t:\\mathcal{M}(\\alpha),\\text{Nodup}(s)\\land\\text{Nodup}(t)\\Rightarrow (s=t\\iff \\forall a, a\\in s\\iff a\\in t).$$$

Lean4

theorem ext {s t : Multiset α} : Nodup s → Nodup t → (s = t ↔ ∀ a, a ∈ s ↔ a ∈ t) :=
  Quotient.inductionOn₂ s t fun _ _ d₁ d₂ => Quotient.eq.trans <| perm_ext_iff_of_nodup d₁ d₂

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