OAI/Combinatorics/SharpRamsey/Marking/MarkingClassSelection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.Marking.expensiveBudget line 16
2. lemma OAI.SharpLogRamsey.Marking.two_expensive_bound line 22
3. lemma OAI.SharpLogRamsey.Marking.twoScan_subset_pointwise line 39
4. def OAI.SharpLogRamsey.Marking.conditionedDeficit line 74
5. theorem OAI.SharpLogRamsey.Marking.actual_common_class_slots line 83
6. theorem OAI.SharpLogRamsey.Marking.twoScan_conditioned_deficit line 123
7. theorem OAI.SharpLogRamsey.Marking.actual_common_class line 142