toMultiset_strictMono — Mathlib

English

Let ι be a type and f,g : ι →₀ ℕ be finitely supported functions with f < g. Then the multiset representation of f is strictly smaller than that of g: toMultiset(f) < toMultiset(g).

Русский

Пусть ι — множества; f,g : ι →₀ ℕ — конечноподдерживаемые функции с f < g. Тогда соответствующее им мультимножество удовлетворяет toMultiset(f) < toMultiset(g).

LaTeX

$$$$ \forall f,g : ι \to_0 \mathbb{N},\ f < g \Rightarrow \operatorname{toMultiset}(f) < \operatorname{toMultiset}(g). $$$$

Lean4

theorem toMultiset_strictMono : StrictMono (@toMultiset ι) := by classical exact (@orderIsoMultiset ι _).strictMono

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