OAI/Probability/SwitchChain/CrossTogglePairs.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.CrossToggle.crossProposal line 17
  2. theorem OAI.Problem315.CrossToggle.crossProposal_left line 22
  3. theorem OAI.Problem315.CrossToggle.crossProposal_right line 32
  4. theorem OAI.Problem315.CrossToggle.crossProposal_swap_pairs line 42
  5. theorem OAI.Problem315.CrossToggle.crossProposal_swap_left line 53
  6. theorem OAI.Problem315.CrossToggle.crossProposal_swap_right line 66
  7. theorem OAI.Problem315.CrossToggle.crossProjection_swap_left line 77
  8. theorem OAI.Problem315.CrossToggle.crossProjection_swap_right line 83
  9. abbrev OAI.Problem315.CrossToggle.VertexPair line 89
  10. def OAI.Problem315.CrossToggle.first line 91
  11. def OAI.Problem315.CrossToggle.second line 94
  12. theorem OAI.Problem315.CrossToggle.first_ne_second line 97
  13. theorem OAI.Problem315.CrossToggle.pair_eq line 100
  14. theorem OAI.Problem315.CrossToggle.endpoints_cases line 103
  15. theorem OAI.Problem315.CrossToggle.endpoints_distinct line 117
  16. def OAI.Problem315.CrossToggle.pairProposal line 128
  17. theorem OAI.Problem315.CrossToggle.pairProposal_symm line 131
  18. theorem OAI.Problem315.CrossToggle.pairProposal_crosses_left line 135
  19. theorem OAI.Problem315.CrossToggle.pairProposal_crosses_right line 140
  20. def OAI.Problem315.CrossToggle.pairProjection line 145
  21. theorem OAI.Problem315.CrossToggle.pairProjection_of_disjoint line 149
  22. theorem OAI.Problem315.CrossToggle.pairProjection_eq_explicit line 153
  23. theorem OAI.Problem315.CrossToggle.pairProjection_symm line 167
  24. theorem OAI.Problem315.CrossToggle.pairProjection_isSymmetric line 175
  25. theorem OAI.Problem315.CrossToggle.pairProjection_idempotent line 184
  26. theorem OAI.Problem315.CrossToggle.pairProjection_mem_left_orthogonal line 191
  27. theorem OAI.Problem315.CrossToggle.pairProjection_mem_right_orthogonal line 199
  28. theorem OAI.Problem315.CrossToggle.pairProjection_mem_common line 205
  29. theorem OAI.Problem315.CrossToggle.pairProjection_energy line 214