Bondy's theorem on induced subsets #
If F is a family of at most |X| distinct finite sets and X is nonempty, some x ∈ X can be
deleted from all of them and they stay distinct (Bondy, 1972; Bondy states it for subsets of an
n-set, the inclusion is not needed). Proof by rank over ZMod 2: if every x ∈ X is bad, choose
A_x ≠ B_x in F with the same erasure; their indicator vectors differ by the unit vector at x.
These |X| unit vectors are linearly independent but lie in the span of the differences
ind C - ind A₀, C ∈ F, of dimension at most |F| - 1 < |X|.
Main results #
Bondy.exists_erase_injOn: at most |X| distinct sets stay distinct after deleting some x in X
References #
- J. A. Bondy, Induced subsets, J. Combin. Theory Ser. B 12 (1972), 201–202.
theorem
Bondy.exists_erase_injOn
{α : Type u_1}
[DecidableEq α]
(X : Finset α)
(hX : X.Nonempty)
(F : Finset (Finset α))
(hcard : F.card ≤ X.card)
:
Bondy's theorem (1972). A family of at most |X| distinct finite sets, X nonempty, has an
element x ∈ X such that deleting x keeps the sets distinct. The sets need not be subsets of X
(Bondy's statement takes subsets of an n-set).