disjoint_finset_sum_right — 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 a (sum_{i∈I} f(i)) holds if and only if for every i ∈ I, Disjoint a (f(i)) holds.

Русский

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

LaTeX

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

Lean4

theorem disjoint_finset_sum_right {i : Finset ι} {f : ι → Multiset α} {a : Multiset α} :
    Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b) := by simpa only [disjoint_comm] using disjoint_finset_sum_left

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