OAI/Combinatorics/SquareDifference/TupleReflection.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.tupleAddressReflect line 10
  2. lemma OAI.SquareDifference.tupleProjection_reflect_all line 19
  3. def OAI.SquareDifference.tupleEntryReflect line 25
  4. lemma OAI.SquareDifference.tupleListEdges_reflect line 29
  5. lemma OAI.SquareDifference.tupleValidity_reflect line 42
  6. lemma OAI.SquareDifference.tupleWeight_reflect line 52
  7. lemma OAI.SquareDifference.tupleOutput_reflect line 67
  8. lemma OAI.SquareDifference.tupleComponent_reflect line 75
  9. lemma OAI.SquareDifference.tupleCutForm_symmetric line 96
  10. def OAI.SquareDifference.symbolPotential line 112
  11. lemma OAI.SquareDifference.symbolPotential_swap line 115
  12. def OAI.SquareDifference.wordPotential line 138
  13. lemma OAI.SquareDifference.wordPotential_reflect line 141
  14. def OAI.SquareDifference.foldWord line 152
  15. lemma OAI.SquareDifference.foldWord_potential_le line 156
  16. lemma OAI.SquareDifference.foldWord_potential_lt line 170
  17. lemma OAI.SquareDifference.exists_unsorted_cut line 184
  18. abbrev OAI.SquareDifference.WordCut line 198
  19. def OAI.SquareDifference.foldMap line 200
  20. lemma OAI.SquareDifference.exists_constant_fold line 204
  21. lemma OAI.SquareDifference.max_fold_preserved line 226
  22. lemma OAI.SquareDifference.word_folding_maximum line 243
  23. def OAI.SquareDifference.graphValidity line 272
  24. lemma OAI.SquareDifference.graphValidity_all line 276
  25. def OAI.SquareDifference.cutInternalEdges line 283
  26. def OAI.SquareDifference.cutCrossEdges line 288
  27. def OAI.SquareDifference.cutCrossDirection line 294
  28. lemma OAI.SquareDifference.cutCrossEdges_factor line 299
  29. lemma OAI.SquareDifference.graphValidity_cut line 321
  30. lemma OAI.SquareDifference.graphValidity_nonneg line 336
  31. lemma OAI.SquareDifference.graphValidity_sq line 340
  32. lemma OAI.SquareDifference.list_quadratic_lower line 350
  33. def OAI.SquareDifference.graphPullback line 375
  34. lemma OAI.SquareDifference.graphValidity_pullback line 380
  35. abbrev OAI.SquareDifference.TupleHalfAddress line 391
  36. abbrev OAI.SquareDifference.TupleHalfEntry line 394
  37. instance OAI.SquareDifference.tupleHalfEntryFintype line 397
  38. def OAI.SquareDifference.tupleEntryHalfEquiv line 404
  39. lemma OAI.SquareDifference.tupleEntryHalfEquiv_inl line 410
  40. lemma OAI.SquareDifference.tupleEntryHalfEquiv_inr line 415
  41. def OAI.SquareDifference.tupleHalfProjection line 431
  42. def OAI.SquareDifference.tupleHalfWeight line 435
  43. def OAI.SquareDifference.tupleUnmarkedGraph line 439
  44. lemma OAI.SquareDifference.tupleUnmarkedGraph_noopp line 443
  45. lemma OAI.SquareDifference.tupleUnmarkedGraph_reflect line 451
  46. lemma OAI.SquareDifference.tupleOutput_half line 461
  47. lemma OAI.SquareDifference.tupleHalfWeight_one_le line 490
  48. lemma OAI.SquareDifference.tupleHalfWeight_le line 495