disjSum_mono_left — Mathlib

English

Disjoint sum is 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 \subseteq t_2 \Rightarrow s.disjSum t_1 \subseteq s.disjSum t_2 $$$

Lean4

theorem disjSum_mono_left (t : Finset β) : Monotone fun s : Finset α => s.disjSum t := fun _ _ hs =>
  disjSum_mono hs Subset.rfl

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