Non-uniform t-intersecting set family

Definition

TIntersecting

by xbgxjack · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsextremal-set-theoryintersecting-familieskatona

A family $\mathcal{A}$ of subsets of a finite ground set is $t$ -intersecting if every two members $A, B \in \mathcal{A}$ (not necessarily distinct) satisfy $|A \cap B| \ge t$ . Taking $A = B$ , this forces every member of the family to have size at least $t$ . This is the non-uniform generalization of an intersecting family (the case $t = 1$ ): the family need not consist of sets of a fixed size, and Katona's 1964 intersection theorem determines the maximum size of such a family in terms of $t$ and the ground set size.

Definition code

import Mathlib

namespace Katona

/-- A family of subsets of a finite type is `t`-intersecting if every pair of members
(including a set intersected with itself) has intersection size at least `t`. -/
def TIntersecting {α : Type*} [DecidableEq α] (t : ℕ) (𝒜 : Finset (Finset α)) : Prop :=
  ∀ A ∈ 𝒜, ∀ B ∈ 𝒜, t ≤ (A ∩ B).card

end Katona

Source

G. O. H. Katona, Intersection theorems for systems of finite sets, Acta Math. Acad. Sci. Hungar. 15 (1964), 329-337.

View graph