OAI/Combinatorics/Hamiltonian/CycleReversal.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Reversal involutions on partners of a fixed incidence state.

  1. theorem OAI.Barnette.cycleCoordinates_of_not_acyclic line 13
  2. theorem OAI.Barnette.TriangleSystem.opposite_indices line 34
  3. structure OAI.Barnette.TriangleSystem.OppositeCycle line 38
  4. theorem OAI.Barnette.TriangleSystem.oppositeCycle_nonempty line 48
  5. theorem OAI.Barnette.TriangleSystem.OppositeCycle.corner_ne line 80
  6. theorem OAI.Barnette.TriangleSystem.OppositeCycle.partner_endpoints line 87
  7. theorem OAI.Barnette.TriangleSystem.OppositeCycle.partner_orientation line 106
  8. def OAI.Barnette.TriangleSystem.OppositeCycle.changedCorners line 127
  9. theorem OAI.Barnette.TriangleSystem.OppositeCycle.changedCorners_image line 131
  10. theorem OAI.Barnette.TriangleSystem.OppositeCycle.changed_assignment_permutation line 136
  11. def OAI.Barnette.TriangleSystem.OppositeCycle.reverse line 171
  12. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reverse_val line 192
  13. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reverse_partner line 195
  14. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reverse_reverse line 208
  15. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reverse_ne line 218
  16. def OAI.Barnette.TriangleSystem.Partners line 229
  17. def OAI.Barnette.TriangleSystem.OppositeCycle.reversal line 235
  18. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reversal_involutive line 238
  19. theorem OAI.Barnette.TriangleSystem.OppositeCycle.reversal_ne line 243