nodup_sup_iff — Mathlib

English

Let α be a type with DecidableEq. For m : Multiset(Multiset α), m.sup is Nodup iff every a ∈ m is Nodup.

Русский

Пусть α имеет разрешимое равенство. Для множества множестv m: Multiset(Multiset α), sup(m) является Nodup тогда и только тогда, когда каждый элемент a ∈ m является Nodup.

LaTeX

$$$$ m.sup.Nodup \\iff \\forall a:\\mathrm{Multiset}(\\alpha),\\ a \\in m \\rightarrow a.Nodup $$$$

Lean4

theorem nodup_sup_iff {α : Type*} [DecidableEq α] {m : Multiset (Multiset α)} :
    m.sup.Nodup ↔ ∀ a : Multiset α, a ∈ m → a.Nodup := by
  induction m using Multiset.induction_on with
  | empty => simp
  | cons _ _ h => simp [h]

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