mem_support_ofMultiset_iff — Mathlib

English

For a ∈ α, a belongs to the support of the PMF from s if and only if a is a member of the finite set of distinct elements of s.

Русский

Пусть a ∈ α. Тогда a принадлежит поддержке PMF, полученной из мультимножества s, тогда и только тогда a принадлежит множеству distinct elements of s.

LaTeX

$$$$ a \\in (\\mathrm{ofMultiset}(s, hs)).\\mathrm{support} \\; \\Longleftrightarrow \\\\ a \\in s^{\\mathrm{toFinset}} $$$$

Lean4

theorem mem_support_ofMultiset_iff (a : α) : a ∈ (ofMultiset s hs).support ↔ a ∈ s.toFinset := by simp

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