ndinter_eq_inter — Mathlib

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 _ _)

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