OAI/Combinatorics/TriangleRemoval/Tracking/PrefixPairClosureBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpTerminalLeave.prefix_pair_closure_budget line 14
2. lemma OAI.SharpTerminalLeave.initial_normalized_pair_bound line 42
3. theorem OAI.SharpTerminalLeave.prefix_pair_barrier_improvement line 57
4. theorem OAI.SharpTerminalLeave.prefix_all_pair_closure line 89