Finite set families and maximal intersection #
This file formalizes the set-family language used in Sections 1 and 4 of
A proof of Chvátal's conjecture via a sharp correlation inequality.
In particular, Family.isMaximalIntersecting_iff and
Family.IsMaximalIntersecting.card_eq give Proposition 4.1. We use mathlib's
Set.Intersecting, IsUpperSet, and IsLowerSet, so intersection includes a
member paired with itself: the empty set cannot belong to an intersecting family.
The dimension-zero exception is explicit. The empty family is maximal intersecting on an empty ground type, but is not antipodal. Accordingly, Proposition 4.1 is stated for a nonempty ground type.
A family of subsets of a finite ground type, representing 𝒜 ⊆ 2^[n]
throughout the paper.
Equations
- Chvatal.Family ι = Finset (Finset ι)
Instances For
The hereditary (decreasing) families of Section 1: taking a subset preserves membership. This is mathlib's lower-set predicate.
Equations
- D.IsHereditary = IsLowerSet ↑D
Instances For
The increasing families of Sections 1–4: taking a superset preserves membership. This is mathlib's upper-set predicate.
Equations
- B.IsIncreasing = IsUpperSet ↑B
Instances For
The intersecting families of Sections 1 and 4: any two members, including a member with itself, have nonempty intersection.
Equations
- B.IsIntersecting = (↑B).Intersecting
Instances For
A maximal intersecting family as defined immediately before Proposition 4.1. Maximality is taken among all families on the given ground type.
Equations
- B.IsMaximalIntersecting = (B.IsIntersecting ∧ ∀ (C : Chvatal.Family ι), C.IsIntersecting → B ⊆ C → B = C)
Instances For
The star D_i = {S ∈ D : i ∈ S} appearing in Chvátal's conjecture
(Theorem 1.1 and Section 4).
Instances For
A star is a subfamily of its ambient family, as used in Theorem 1.1.
Every star is intersecting; this is the last observation in the proof of Proposition 5.3, and explains why stars are competitors in Chvátal's conjecture.
Intersecting families cannot contain the empty set (Section 4's convention).
Membership in an intersecting family guarantees that the member is nonempty, including when the two members in the definition coincide.
An intersecting subfamily remains intersecting; this is used when restricting a maximal intersecting family to a hereditary family in Section 4.
Every intersecting family has a maximal intersecting extension, as used at the end of Section 4 and in the proof of Proposition 5.3. This also holds in dimension zero.
The first assertion in the proof of Proposition 4.1: adjoining supersets preserves intersection, so every maximal intersecting family is increasing.
Family duality is an involution, as is the Boolean-function duality in Sections 1–3.
A family is antipodal when exactly one of each complementary pair belongs to it, as defined immediately before Proposition 4.1.
Instances For
Antipodality is the self-duality condition used in Section 4.
Duality preserves increasing families, as used for 𝒢* in Section 3.
Complementing membership in a hereditary family gives an increasing family;
this is the family underlying f = 1 - 𝟙_D in Section 4.
The cardinality bound for intersecting families used by Proposition 4.1, written without division so it remains valid in dimension zero.
The equality case in Proposition 4.1, in the division-free form
2 |B| = 2^n. The ground type must be nonempty.
Proposition 4.1: a maximal intersecting family occupies half the cube.
The antipodality conclusion of Proposition 4.1, obtained by counting the disjoint family and its image under complementation.
The converse direction of Proposition 4.1: increasing antipodal families are intersecting.
The converse maximality assertion of Proposition 4.1: any newly adjoined member has its complement already in the original family.
Proposition 4.1: on a nonempty ground type, maximal intersecting families are exactly the increasing antipodal families.
A full-cube star is increasing, as used among the examples in Section 5.
A full-cube star selects exactly one member of each complementary pair; this is the simplest antipodal family in Proposition 4.1.
Full-cube stars are maximal intersecting, the basic extremal examples in Sections 4 and 5.
The last reduction in Section 4: to prove the star bound inside D, it
suffices to bound D ∩ B for each maximal intersecting family B. This lemma
isolates the purely combinatorial reduction from the correlation inequality.