disjSum_mono_right — Mathlib

English

For a fixed s, the map t ↦ s.disjSum t is monotone with respect to ≤ on multisets.

Русский

Для фиксированного s отображение t ↦ s.disjSum t монотонно по отношению к ≤ на мультимножествах.

LaTeX

$$$ (\\text{Monotone } (\\lambda t. s.disjSum t)) $$$

Lean4

theorem disjSum_mono_right (s : Multiset α) : Monotone (s.disjSum : Multiset β → Multiset (α ⊕ β)) := fun _ _ ht =>
  Multiset.add_le_add_left (map_le_map ht)

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