mem_ndinter — Mathlib

English

For multisets s,t and element a, a ∈ ndinter s t iff a ∈ s and a ∈ t.

Русский

Для мультимножества s,t и элемента a: a ∈ ndinter s t тогда и только тогда, когда a ∈ s и a ∈ t.

LaTeX

$$$a \\in \\mathrm{ndinter}(s,t) \\iff a \\in s \\land a \\in t$$$

Lean4

@[simp]
theorem mem_ndinter {s t : Multiset α} {a : α} : a ∈ ndinter s t ↔ a ∈ s ∧ a ∈ t := by
  simp [ndinter, mem_filter]
    -- simp can prove this once we have `ndinter_eq_inter` and `Nodup.inter` a few lines down.

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