pairwise_disjoint_powersetCard — Mathlib

English

For a fixed s, the family { powersetCard i s } has pairwise disjoint elements: for i ≠ j, the multisets are disjoint.

Русский

Для фиксированного s множество { powersetCard i s } попарно диссоциирует: при i ≠ j множества диссоциированы.

LaTeX

$$$\_root_.Pairwise (\nspace f) \; (i,j) \mapsto \mathrm{Disjoint}(s.\mathrm{powersetCard} i, s.\mathrm{powersetCard} j)$$$

Lean4

theorem pairwise_disjoint_powersetCard (s : Multiset α) :
    _root_.Pairwise fun i j => Disjoint (s.powersetCard i) (s.powersetCard j) := fun _ _ h ↦
  disjoint_left.mpr fun hi hj ↦ h ((Multiset.mem_powersetCard.mp hi).2.symm.trans (Multiset.mem_powersetCard.mp hj).2)

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