OAI/Combinatorics/TriangleRemoval/Process/HistoryGraphNested.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpTerminalLeave.history_graph_nested line 15
2. lemma OAI.SharpTerminalLeave.densityEdgeSafe_centered_bound line 25
3. lemma OAI.SharpTerminalLeave.densityEdgeSafe_pair_upper line 39
4. lemma OAI.SharpTerminalLeave.initial_centered_edge_bound line 47
5. lemma OAI.SharpTerminalLeave.prefix_triangle_radius_small line 61
6. theorem OAI.SharpTerminalLeave.prefix_edge_coefficient_bounds line 70
7. theorem OAI.SharpTerminalLeave.prefix_edge_forcing_bound line 114