inter_le_ndinter — Mathlib

English

Let s and t be multisets over a type α. Then the usual intersection s ∩ t is a submultiset of the ndinter s t; i.e., every element appears in s ∩ t no more times than in ndinter s t.

Русский

Пусть s и t — мультимножества над типом α. Тогда обычное пересечение s ∩ t является подпmultiset ndinter s t; то есть в s ∩ t каждое значение встречается не чаще, чем в ndinter s t.

LaTeX

$$$s \cap t \le \mathrm{ndinter}(s,t)$$$

Lean4

theorem inter_le_ndinter (s t : Multiset α) : s ∩ t ≤ ndinter s t :=
  le_ndinter.2 ⟨inter_le_left, subset_of_le inter_le_right⟩

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