### Abstract

The Sauer-Shelah Lemma is a fundamental result in extremal set theory and combinatorics. It guarantees the existence of a set $T$ of size $k$ that is shattered by a family of sets $\mathcal{F}$ if the cardinality of the family is greater than some bound dependent on $k$. A set $T$ is said to be shattered by a family $\mathcal{F}$ if every subset of $T$ can be obtained as an intersection of $T$ with some set $S \in \mathcal{F}$. The Sauer-Shelah Lemma has found use in diverse fields such as computational geometry, approximation algorithms and machine learning. In this entry we formalize the notion of shattering and prove the generalized and standard versions of the Sauer-Shelah Lemma.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Sauer_Shelah_Lemma

- Shattering
- Card_Lemmas
- Binomial_Lemmas
- Sauer_Shelah_Lemma

## Cite

×

Sauer_Shelah_Lemma-AFP

    @article{Sauer_Shelah_Lemma-AFP,
      author  = {Ata Keskin},
      title   = {Sauer-Shelah Lemma},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Sauer_Shelah_Lemma.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Nov 28, 2022 : Isabelle2022