disjSum_strictMono_right — Mathlib

English

Strictly monotone in the right argument: if t1 ⊂ t2 then s.disjSum t1 ⊂ s.disjSum t2.

Русский

Строго монотонно справа: если t1 ⊂ t2, то s.disjSum t1 ⊂ s.disjSum t2.

LaTeX

$$$ t_1 \subset t_2 \Rightarrow s.disjSum t_1 \subset s.disjSum t_2 $$$

Lean4

theorem disjSum_strictMono_right (s : Finset α) : StrictMono (s.disjSum : Finset β → Finset (α ⊕ β)) := fun _ _ =>
  disjSum_ssubset_disjSum_of_subset_of_ssubset Subset.rfl

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