OAI/Combinatorics/RamseyFive/Entropy/MarkedActualBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.Marking.actual_marked_deficit line 21
2. lemma OAI.SharpRamseyFive.FiniteEntropy.fiber_pair_source line 91
3. lemma OAI.SharpRamseyFive.FiniteEntropy.pair_fiber_domains line 100
4. lemma OAI.SharpRamseyFive.FiniteEntropy.pair_fiber_pred line 109
5. lemma OAI.SharpRamseyFive.FiniteEntropy.pair_map_tuple line 116
6. lemma OAI.SharpRamseyFive.FiniteEntropy.fiber_pair_map line 121
7. def OAI.SharpRamseyFive.FiniteEntropy.ContextDescription.boundedDomain line 139
8. lemma OAI.SharpRamseyFive.FiniteEntropy.ContextDescription.boundedDomain_cap line 142
9. lemma OAI.SharpRamseyFive.FiniteEntropy.ContextDescription.boundedDomain_contains line 151