OAI/Combinatorics/RamseyFive/Entropy/SubsetDeficit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.entropy_subset_split line 16
2. theorem OAI.SharpRamseyFive.FiniteEntropy.subset_deficit_le_active line 38
3. abbrev OAI.SharpRamseyFive.FiniteEntropy.UnionTranscript line 72
4. def OAI.SharpRamseyFive.FiniteEntropy.unionMessage line 75
5. def OAI.SharpRamseyFive.FiniteEntropy.unspecified line 79
6. lemma OAI.SharpRamseyFive.FiniteEntropy.unspecified_unionMessage line 83
7. lemma OAI.SharpRamseyFive.FiniteEntropy.unspecified_card line 92
8. lemma OAI.SharpRamseyFive.FiniteEntropy.unionMessage_fixedOutside line 99
9. theorem OAI.SharpRamseyFive.FiniteEntropy.union_deficit_bound line 117