OAI/Combinatorics/MatchingCount/Graphs/FirstHoleSortedCons.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.Subdivision.first_hole_of_sorted_cons line 12
2. lemma OAI.MatchingFPRAS.Subdivision.last_hole_of_sorted_append line 25
3. theorem OAI.MatchingFPRAS.Subdivision.HoleBlocks.left_uses line 39
4. theorem OAI.MatchingFPRAS.Subdivision.HoleBlocks.right_uses line 68
5. theorem OAI.MatchingFPRAS.Subdivision.HoleBlocks.neutral_lt line 98
6. lemma OAI.MatchingFPRAS.Subdivision.HoleBlocks.flatten_nodup line 107
7. lemma OAI.MatchingFPRAS.Subdivision.HoleBlocks.left_mem line 110
8. lemma OAI.MatchingFPRAS.Subdivision.HoleBlocks.right_mem line 117
9. lemma OAI.MatchingFPRAS.Subdivision.HoleBlocks.neutral_mem line 124
10. lemma OAI.MatchingFPRAS.Subdivision.HoleBlocks.reorder line 135
11. lemma OAI.MatchingFPRAS.Subdivision.HoleBlocks.reordered_nodup line 140
12. lemma OAI.MatchingFPRAS.Subdivision.uses_not_hole line 150
13. lemma OAI.MatchingFPRAS.Subdivision.uses_unique line 155
14. lemma OAI.MatchingFPRAS.Subdivision.left_consumes line 161
15. lemma OAI.MatchingFPRAS.Subdivision.right_consumes line 172
16. lemma OAI.MatchingFPRAS.Subdivision.internalStrength_le_twice_incident line 182
17. lemma OAI.MatchingFPRAS.Subdivision.profile_adjacent_near line 217