OAI/Combinatorics/RamseyFive/Entropy/LocalNodeLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.FiniteEntropy.pairOptions line 12
2. lemma OAI.SharpRamseyFive.FiniteEntropy.pairOptions_none line 15
3. lemma OAI.SharpRamseyFive.FiniteEntropy.pairOptions_positive line 22
4. def OAI.SharpRamseyFive.ProjectiveIncidence.producedPairLaw line 37
5. def OAI.SharpRamseyFive.ProjectiveIncidence.localNodeLaw line 52
6. lemma OAI.SharpRamseyFive.ProjectiveIncidence.producedPairLaw_spec line 59
7. theorem OAI.SharpRamseyFive.ProjectiveIncidence.eventually_local_node line 86