OAI/Combinatorics/SharpRamsey/Execution/ExecutedPotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.ExecutedPotential.potential line 15
2. lemma OAI.SharpLogRamsey.ExecutedPotential.potential_nonneg line 18
3. lemma OAI.SharpLogRamsey.ExecutedPotential.cap_potential_zero_allowed line 20
4. theorem OAI.SharpLogRamsey.ExecutedPotential.branch line 29
5. def OAI.SharpLogRamsey.ExecutedPotential.annotate line 68
6. lemma OAI.SharpLogRamsey.ExecutedPotential.erase_annotate line 78
7. lemma OAI.SharpLogRamsey.ExecutedPotential.annotate_height line 86
8. lemma OAI.SharpLogRamsey.ExecutedPotential.annotate_numNodes line 98
9. lemma OAI.SharpLogRamsey.ExecutedPotential.root_le line 110
10. theorem OAI.SharpLogRamsey.ExecutedPotential.admissible line 122