le_dedup — Mathlib

English

For any s,t, s ≤ dedup t if and only if s ≤ t and s is Nodup.

Русский

Для любых s,t верно: s ≤ dedup(t) тогда и только тогда, когда s ≤ t и s без повторов.

LaTeX

$$$$s \le dedup(t) \iff (s \le t) \land Nodup(s)$$$$

Lean4

theorem le_dedup {s t : Multiset α} : s ≤ dedup t ↔ s ≤ t ∧ Nodup s :=
  ⟨fun h => ⟨le_trans h (dedup_le _), nodup_of_le h (nodup_dedup _)⟩, fun ⟨l, d⟩ =>
    (le_iff_subset d).2 <| Subset.trans (subset_of_le l) (subset_dedup _)⟩

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