OAI/Combinatorics/SharpRamsey/Reciprocal/ProdRectangleEvent.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.Selection.Law.prod_rectangle_event line 14
  2. lemma OAI.SharpLogRamsey.Selection.Law.event_filter_le_add line 19
  3. def OAI.SharpLogRamsey.Selection.firstCore line 29
  4. def OAI.SharpLogRamsey.Selection.secondCore line 32
  5. def OAI.SharpLogRamsey.Selection.coreContained line 35
  6. def OAI.SharpLogRamsey.Selection.coreCollision line 39
  7. lemma OAI.SharpLogRamsey.Selection.core_capture_product line 45
  8. lemma OAI.SharpLogRamsey.Selection.core_collision_capture line 62
  9. lemma OAI.SharpLogRamsey.Selection.exceptional_core_mass line 90
  10. theorem OAI.SharpLogRamsey.Selection.reciprocal_incidence_collision line 123
  11. lemma OAI.SharpLogRamsey.Selection.not_contained_of_rank_sum line 178
  12. lemma OAI.SharpLogRamsey.Selection.complementary_of_rank_sum line 186
  13. lemma OAI.SharpLogRamsey.Selection.firstCore_own line 205
  14. lemma OAI.SharpLogRamsey.Selection.secondCore_own line 221
  15. def OAI.SharpLogRamsey.Selection.orthogonalRectangle line 236
  16. lemma OAI.SharpLogRamsey.Selection.coreCollision_rectangle line 240
  17. lemma OAI.SharpLogRamsey.Selection.Law.event_map line 268
  18. lemma OAI.SharpLogRamsey.Selection.slot_flag line 278
  19. theorem OAI.SharpLogRamsey.Selection.reciprocal_charge_sum line 286