disjoint_sum_right — Mathlib

English

For a Multiset a and a List of Multisets l, Disjoint a l.sum holds iff ∀ b ∈ l, Disjoint a b.

Русский

Для мультисека a и списка l мультимножеств, Disjoint a l.sum эквивалентно ∀ b ∈ l, Disjoint a b.

LaTeX

$$$$\text{Disjoint } a\, l.sum \iff \forall b \in l,\; \text{Disjoint } a\, b.$$$$

Lean4

theorem disjoint_sum_right {a : Multiset α} {i : Multiset (Multiset α)} : Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b := by
  simpa only [disjoint_comm (a := a)] using disjoint_sum_left

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