OAI/NumberTheory/Ostmann/Conclusion/OverlapComponents.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Conclusion.overlapRelation line 9
2. def OAI.Ostmann.Conclusion.OverlapComponent line 12
3. instance OAI.Ostmann.Conclusion.(instance at line 15) line 15
4. instance OAI.Ostmann.Conclusion.(instance at line 19) line 19
5. instance OAI.Ostmann.Conclusion.(instance at line 22) line 22
6. def OAI.Ostmann.Conclusion.leftComponent line 25
7. def OAI.Ostmann.Conclusion.rightComponent line 28
8. theorem OAI.Ostmann.Conclusion.leftComponent_surjective line 32
9. theorem OAI.Ostmann.Conclusion.slot_component line 36
10. theorem OAI.Ostmann.Conclusion.component_card_balance line 43
11. theorem OAI.Ostmann.Conclusion.component_card_pos line 54
12. theorem OAI.Ostmann.Conclusion.component_cards_sum line 59
13. theorem OAI.Ostmann.Conclusion.overlapComponent_card_le line 64
14. theorem OAI.Ostmann.Conclusion.component_matching_card line 69
15. def OAI.Ostmann.Conclusion.BadArrangement line 76