Proof of `Bounded VC-dimension of monadically dependent classes`
groundedproofs/Lax185574Proofs/BoundedVCClasses.lean · lax-185574
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
In the paper
- page 13 of this submission's paper
Description
A monadically dependent class has bounded VC-dimension, since otherwise the edge formula has the independence property on it.
The argument is carried out for the graph classes of the archive and their monadic dependence, and transferred to the graph classes used here.