toMultiset_sup — Mathlib

English

For f,g : α →₀ ℕ, the supremum (pointwise maximum) corresponds to the multiset union: toMultiset(f ⊔ g) = toMultiset f ∪ toMultiset g.

Русский

Для функций f,g : α →₀ ℕ верхняя грань по точкам соответствует объединению мультимножества: toMultiset(f ⊔ g) = toMultiset f ∪ toMultiset g.

LaTeX

$$$\mathrm{toMultiset}(f \sqcup g) = \mathrm{toMultiset}(f) \cup \mathrm{toMultiset}(g)$$$

Lean4

theorem toMultiset_sup [DecidableEq α] (f g : α →₀ ℕ) : toMultiset (f ⊔ g) = toMultiset f ∪ toMultiset g :=
  by
  ext
  simp_rw [Multiset.count_union, Finsupp.count_toMultiset, Finsupp.sup_apply]

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