OAI/Combinatorics/IndependentSets/Expansion/PoweringWalks.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.PortGraph line 7
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.Edge line 11
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.Walk line 12
  4. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.next line 16
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rot_rot line 18
  6. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.walkEnd line 21
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.walkEnd_nil line 25
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.walkEnd_cons line 27
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.walkEnd_append line 30
  10. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.splitHead line 36
  11. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rotateHead line 47
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rotateHead_vertex line 51
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rotateHead_zero line 54
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rotateHead_succ line 57
  15. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.permutePorts line 61
  16. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.wordEnd line 75
  17. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.endpoint line 79
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.natCard_walk line 82
  19. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.headTailEquiv line 86
  20. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.advanceTail line 97
  21. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.edgeAt line 100
  22. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.pivotEquiv line 106
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.pivotEquiv_fst line 116
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.edgeAt_port line 130
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.pivotEquiv_zero_apply line 146
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.pivotEquiv_succ_apply line 150
  27. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.projectedFiberEquiv line 157
  28. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.projectedEventEquiv line 169
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_fiber line 187
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_event line 196
  31. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.leftFromPivot line 206
  32. def OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rightFromPivot line 212
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.leftFromPivot_zero line 219
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rightFromPivot_zero line 223
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.leftFromPivot_actual line 228
  36. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringWalks.rightFromPivot_actual line 247