pairwise_disjoint_powersetCard — Mathlib

English

For any s, the family of sets s.powersetCard i over i is pairwise disjoint.

Русский

Для любого s множество s.powersetCard i по i образуют попарно непересекающиеся множества.

LaTeX

$$Pairwise (fun i j => Disjoint (powersetCard i s) (powersetCard j s))$$

Lean4

theorem pairwise_disjoint_powersetCard (s : Finset α) :
    Pairwise fun i j => Disjoint (s.powersetCard i) (s.powersetCard j) := fun _i _j hij =>
  Finset.disjoint_left.mpr fun _x hi hj => hij <| (mem_powersetCard.mp hi).2.symm.trans (mem_powersetCard.mp hj).2

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