toMultiset_inf — Mathlib

English

For f,g : α →₀ ℕ, the infimum corresponds to multiset intersection: toMultiset(f ⊓ g) = toMultiset f ∩ toMultiset g.

Русский

Для f,g : α →₀ ℕ пересечение соответствует пересечению мультимножества: toMultiset(f ⊓ g) = toMultiset f ∩ toMultiset g.

LaTeX

$$$\mathrm{toMultiset}(f \sqcap g) = \mathrm{toMultiset}(f) \cap \mathrm{toMultiset}(g)$$$

Lean4

theorem toMultiset_inf [DecidableEq α] (f g : α →₀ ℕ) : toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g :=
  by
  ext
  simp_rw [Multiset.count_inter, Finsupp.count_toMultiset, Finsupp.inf_apply]

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