English
If s has no duplicate elements (is nodup), then ndinter s t coincides with the ordinary intersection s ∩ t.
Русский
Если множество элементов s не содержит повторений (s есть без дублей), то ndinter s t совпадает с обычным пересечением s ∩ t.
LaTeX
$$s \text{ Nodup } \Rightarrow ndinter\,s\,t = s \cap t$$
Lean4
@[simp]
theorem ndinter_eq_inter {s t : Multiset α} (d : Nodup s) : ndinter s t = s ∩ t :=
le_antisymm (le_inter (ndinter_le_left _ _) (ndinter_le_right _ d)) (inter_le_ndinter _ _)