disjoint_sum_left — 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_left {a : Multiset α} {i : Multiset (Multiset α)} : Disjoint i.sum a ↔ ∀ b ∈ i, Disjoint b a :=
  Quotient.inductionOn i fun l => by
    rw [quot_mk_to_coe, Multiset.sum_coe]
    exact disjoint_list_sum_left

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