toMultiset_sup — Mathlib

English

toMultiset supremum corresponds to Multiset union: toMultiset(f ⊔ g) = toMultiset f ∪ toMultiset g.

Русский

supremum соответствует объединению мультимножест: toMultiset(f ⊔ g) = toMultiset f ∪ toMultiset g.

LaTeX

$$$$ \\operatorname{toMultiset}(f \\sup g) = \\operatorname{toMultiset}(f) \\cup \\operatorname{toMultiset}(g) $$$$

Lean4

@[simp]
theorem toMultiset_sup : toMultiset (f ⊔ g) = toMultiset f ∪ toMultiset g :=
  Multiset.toDFinsupp_injective <| by simp

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