OAI/Combinatorics/BalancedRyser/Local/AlignedUsedTestTransport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.Local.UsedEventUnion.usedGeometricGuards line 15
2. theorem OAI.Balanced.Local.UsedEventUnion.admissible_usedGeometricGuards line 22
3. theorem OAI.Balanced.Local.UsedEventUnion.usedGeometricGuards_agree line 33
4. def OAI.Balanced.Local.UsedEventUnion.geometricUsedTest line 45
5. def OAI.Balanced.Local.UsedEventUnion.geometricCollinearTest line 52
6. theorem OAI.Balanced.Local.UsedEventUnion.usedConstituentTest_implies_geometric line 67
7. theorem OAI.Balanced.Local.UsedEventUnion.collinearTest_implies_geometric line 74
8. theorem OAI.Balanced.Local.UsedEventUnion.geometricUsedTest_agree line 82
9. theorem OAI.Balanced.Local.UsedEventUnion.geometricCollinearTest_agree line 93
10. theorem OAI.Balanced.Local.UsedEventUnion.conditioned_usedTest_le_uniform_free line 105
11. theorem OAI.Balanced.Local.UsedEventUnion.conditioned_collinearTest_le_uniform_free line 119