disjoint_list_sum_left — Mathlib

English

For a Multiset a and a list l of multisets, Disjoint a l.sum holds iff every b in l is Disjoint a b.

Русский

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

LaTeX

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

Lean4

theorem disjoint_list_sum_left {a : Multiset α} {l : List (Multiset α)} : Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a := by
  induction l with
  | nil => simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
  | cons b bs ih => simp [ih]

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