mem_toMultiset — Mathlib

English

For f : α →₀ ℕ and i ∈ α, i is in toMultiset f iff i is in the support of f.

Русский

Для f : α →₀ ℕ и i ∈ α верно: i ∈ toMultiset f ⇔ i ∈ поддержка f.

LaTeX

$$$i \in \mathrm{toMultiset}(f) \;\iff\; i \in \mathrm{support}(f)$$$

Lean4

@[simp]
theorem mem_toMultiset (f : α →₀ ℕ) (i : α) : i ∈ toMultiset f ↔ i ∈ f.support := by
  classical rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]

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