mem_sub_of_nodup — Mathlib

English

If s is Nodup, then a ∈ s − t iff a ∈ s and a ∉ t.

Русский

Если s является Nodup, то a ∈ s − t тогда и только тогда a ∈ s и a ∉ t.

LaTeX

$$$$ s \text{ Nodup } \Rightarrow a \in s - t \iff a \in s \land a \notin t $$$$

Lean4

theorem mem_sub_of_nodup [DecidableEq α] {a : α} {s t : Multiset α} (d : Nodup s) : a ∈ s - t ↔ a ∈ s ∧ a ∉ t :=
  ⟨fun h =>
    ⟨mem_of_le (Multiset.sub_le_self ..) h, fun h' =>
      by
      refine count_eq_zero.1 ?_ h
      rw [count_sub a s t, Nat.sub_eq_zero_iff_le]
      exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')⟩,
    fun ⟨h₁, h₂⟩ => Or.resolve_right (mem_add.1 <| mem_of_le Multiset.le_sub_add h₁) h₂⟩

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