toFinsupp_strictMono — Mathlib

English

The map from Multiset to Finsupp, sending a multiset to the function counting multiplicities, is strictly monotone: Multiset.toFinsupp is StrictMono.

Русский

Отображение Multiset → Finsupp, считающее кратности элементов, строго монотонно.

LaTeX

$$$$ \text{StrictMono}(\operatorname{Multiset.toFinsupp}_{ι}). $$$$

Lean4

theorem toFinsupp_strictMono [DecidableEq ι] : StrictMono (@Multiset.toFinsupp ι _) :=
  (@Finsupp.orderIsoMultiset ι).symm.strictMono

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