disjSum_mono_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem disjSum_mono_left (t : Multiset β) : Monotone fun s : Multiset α => s.disjSum t := fun _ _ hs =>
  Multiset.add_le_add_right (map_le_map hs)

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