toMultiset_inf — Mathlib

English

toMultiset infimum corresponds to Finset intersection: toMultiset(f ⊓ g) = toMultiset f ∩ toMultiset g.

Русский

infimum соответствует пересечению: toMultiset(f ⊓ g) = toMultiset f ∩ toMultiset g.

LaTeX

$$$$ \\operatorname{toMultiset}(f \\inf g) = \\operatorname{toMultiset}(f) \\cap \\operatorname{toMultiset}(g) $$$$

Lean4

@[simp]
theorem toMultiset_inf : toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g :=
  Multiset.toDFinsupp_injective <| by simp

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