disjoint_finset_sum_left — Mathlib

English

Let I be a finite index set and for each i ∈ I let f(i) be a multiset of α; let a be a fixed multiset of α. Then Disjoint (sum_{i∈I} f(i)) a holds if and only if for every i ∈ I, Disjoint (f(i)) a holds.

Русский

Пусть I — конечное множество индексов, и для каждого i ∈ I f(i) — мультсет над α; пусть a — фиксированная мультсет над α. Тогда несовместность (Disjoint) ∑_{i∈I} f(i) с a эквивалентна несовместности каждого f(i) с a для всех i ∈ I.

LaTeX

$$$\operatorname{Disjoint}\left(\sum_{i \in I} f(i), a\right) \iff \forall i \in I,\ \operatorname{Disjoint}\left(f(i), a\right)$$$

Lean4

theorem disjoint_finset_sum_left {i : Finset ι} {f : ι → Multiset α} {a : Multiset α} :
    Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a :=
  by
  convert @disjoint_sum_left _ a (map f i.val)
  simp

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