OAI/Probability/SwitchChain/PairFiber.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.PairFiber.Outside line 12
  2. def OAI.Problem315.PairFiber.edgeBit line 14
  3. def OAI.Problem315.PairFiber.key line 18
  4. def OAI.Problem315.PairFiber.singletonSet line 23
  5. def OAI.Problem315.PairFiber.leftSet line 27
  6. def OAI.Problem315.PairFiber.commonSet line 31
  7. theorem OAI.Problem315.PairFiber.mem_singletonSet line 35
  8. theorem OAI.Problem315.PairFiber.mem_leftSet line 40
  9. theorem OAI.Problem315.PairFiber.mem_commonSet line 45
  10. theorem OAI.Problem315.PairFiber.leftSet_subset_singletonSet line 50
  11. theorem OAI.Problem315.PairFiber.key_count line 57
  12. theorem OAI.Problem315.PairFiber.key_internal line 65
  13. theorem OAI.Problem315.PairFiber.key_outside line 72
  14. theorem OAI.Problem315.PairFiber.singletonSet_eq_of_key_eq line 81
  15. theorem OAI.Problem315.PairFiber.commonSet_eq_of_key_eq line 90
  16. theorem OAI.Problem315.PairFiber.key_left_adj line 99
  17. theorem OAI.Problem315.PairFiber.key_right_adj line 111
  18. theorem OAI.Problem315.PairFiber.graph_eq_of_key_leftSet_eq line 122
  19. theorem OAI.Problem315.PairFiber.key_swap line 150
  20. def OAI.Problem315.PairFiber.assemble line 162
  21. theorem OAI.Problem315.PairFiber.assemble_adj_left line 193
  22. theorem OAI.Problem315.PairFiber.assemble_adj_right line 201
  23. theorem OAI.Problem315.PairFiber.assemble_adj_internal line 209
  24. theorem OAI.Problem315.PairFiber.assemble_adj_outside line 219
  25. def OAI.Problem315.PairFiber.trade line 227
  26. theorem OAI.Problem315.PairFiber.trade_adj_left line 241
  27. theorem OAI.Problem315.PairFiber.trade_adj_right line 250
  28. theorem OAI.Problem315.PairFiber.trade_adj_internal line 260
  29. theorem OAI.Problem315.PairFiber.trade_adj_outside line 266
  30. theorem OAI.Problem315.PairFiber.key_eq_of line 274
  31. theorem OAI.Problem315.PairFiber.key_trade line 290
  32. theorem OAI.Problem315.PairFiber.leftSet_trade line 317