disjSum_mono — Mathlib

English

Disjoint sum is monotone in the left argument: if s1 ⊆ s2, then s1.disjSum t ⊆ s2.disjSum t.

Русский

Дизъюнктная сумма монотонна по левой аргументации: если s1 ⊆ s2, то s1.disjSum t ⊆ s2.disjSum t.

LaTeX

$$$ s_1 \subseteq s_2 \Rightarrow s_1.disjSum t \subseteq s_2.disjSum t $$$

Lean4

theorem disjSum_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁.disjSum t₁ ⊆ s₂.disjSum t₂ :=
  val_le_iff.1 <| Multiset.disjSum_mono (val_le_iff.2 hs) (val_le_iff.2 ht)

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