pairwise_disjoint_gammaSet — Mathlib

English

For fixed N and r, the family {gammaSet(N,r,a)} as a varies over all a is pairwise disjoint: any two distinct a give disjoint sets.

Русский

Для фиксированного N и r семейство {gammaSet(N,r,a)} по всем a попарно не пересекается: при разных a множества не пересекаются.

LaTeX

$$Pairwise(Disjoint on gammaSet(N,r)).$$

Lean4

theorem pairwise_disjoint_gammaSet : Pairwise (Disjoint on gammaSet N r) :=
  by
  refine fun u v huv ↦ ?_
  contrapose! huv
  obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv
  exact hf.1.1.symm.trans hf.2.1

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