val_strictMono — Mathlib

English

The map taking a Finset to its underlying Multiset is strictly monotone with respect to inclusion.

Русский

Отображение, отправляющее конечное множество в соответствующее мультимножество, строго монотонно по включению.

LaTeX

$$$\operatorname{StrictMono}(\mathrm{val}: \mathrm{Finset} \alpha \to \mathrm{Multiset}\alpha)$$$

Lean4

theorem val_strictMono : StrictMono (val : Finset α → Multiset α) := fun _ _ ↦ val_lt_iff.2

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