support_ofMultiset — Mathlib

English

For a nonzero multiset s, the support of the PMF built from s is exactly the set of distinct elements of s.

Русский

Для непустого мультимножества s поддержка вероятностной массы, полученной из s, совпадает с множеством всех различных элементов s.

LaTeX

$$$$ \\operatorname{supp}(\\mathrm{ofMultiset}(s, hs)) = s^{\\mathrm{toFinset}} $$$$

Lean4

@[simp]
theorem support_ofMultiset : (ofMultiset s hs).support = s.toFinset :=
  Set.ext (by simp [mem_support_iff])

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