noncomputable def BollobasTwoFamilies.goodPerms {α : Type u_1} [DecidableEq α] [Fintype α] (S T : Finset α) : Finset (Equiv.Perm α)

goodPerms S T is the set of permutations σ of α such that every element of S appears before every element of T in the linear ordering induced by σ.

theorem BollobasTwoFamilies.disjoint_goodPerms {α : Type u_1} [DecidableEq α] [Fintype α] {S₁ T₁ S₂ T₂ : Finset α} (h₁ : (S₁ ∩ T₂).Nonempty) (h₂ : (S₂ ∩ T₁).Nonempty) : Disjoint (goodPerms S₁ T₁) (goodPerms S₂ T₂)

If S₁ ∩ T₂ and S₂ ∩ T₁ are both nonempty, the sets of good permutations for (S₁, T₁) and (S₂, T₂) are disjoint, since a common permutation would force a cyclic ordering contradiction.

theorem BollobasTwoFamilies.card_goodPerms_mul_choose {α : Type u_1} [DecidableEq α] [Fintype α] (S T : Finset α) (hST : Disjoint S T) : (goodPerms S T).card * (S.card + T.card).choose S.card = (Fintype.card α).factorial

For disjoint sets S, T ⊆ α, the number of permutations placing S before T times $\binom{|S|+|T|}{|S|}$ equals $|\alpha|!$.

theorem BollobasTwoFamilies.choose_pos_of_add (a b : ℕ) : 0 < (a + b).choose a

The binomial coefficient $\binom{a+b}{a}$ is positive.

theorem BollobasTwoFamilies.bollobas_two_families {α : Type u_1} [DecidableEq α] [Fintype α] {m : ℕ} (A B : Fin m → Finset α) (cross : ∀ (i j : Fin m), A i ∩ B j = ∅ ↔ i = j) : ∑ i : Fin m, (↑(((A i).card + (B i).card).choose (A i).card))⁻¹ ≤ 1

(Theorem 1.2.4, Bollobás Two Families Theorem, weighted form) Given families $(A_i)_{i < m}$ and $(B_i)_{i < m}$ with $A_i \cap B_j = \varnothing$ iff $i = j$, then $$\sum_{i < m} \binom{|A_i| + |B_i|}{|A_i|}^{-1} \le 1.$$

theorem BollobasTwoFamilies.bollobas_two_families_uniform {α : Type u_1} [DecidableEq α] [Fintype α] {m a b : ℕ} (A B : Fin m → Finset α) (hA : ∀ (i : Fin m), (A i).card = a) (hB : ∀ (i : Fin m), (B i).card = b) (cross : ∀ (i j : Fin m), A i ∩ B j = ∅ ↔ i = j) : m ≤ (a + b).choose a

(Theorem 1.2.6, Bollobás Two Families Theorem, uniform form) If all A i have size a and all B i have size b, the cross condition implies $m \le \binom{a+b}{a}$.