OAI/Combinatorics/BalancedRyser/Local/ChildAlignment.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.TupleAlignment.ChildOffsets line 10
  2. def OAI.Balanced.TupleAlignment.childFreshEquiv line 13
  3. theorem OAI.Balanced.TupleAlignment.tuplePositionEquiv_symm_apply line 24
  4. theorem OAI.Balanced.TupleAlignment.lineEvalEquiv_symm_fst line 31
  5. theorem OAI.Balanced.TupleAlignment.lineEvalEquiv_symm_snd line 35
  6. def OAI.Balanced.TupleAlignment.childAlignedPositions line 39
  7. theorem OAI.Balanced.TupleAlignment.childAlignedPositions_onLine line 46
  8. abbrev OAI.Balanced.TupleAlignment.AlignedChildOffsets line 55
  9. def OAI.Balanced.TupleAlignment.alignedChildFromPair line 61
  10. theorem OAI.Balanced.TupleAlignment.alignedChildFromPair_positions line 83
  11. theorem OAI.Balanced.TupleAlignment.tuplePosition_lineEval_left line 90
  12. theorem OAI.Balanced.TupleAlignment.tuplePosition_lineEval_right line 96
  13. def OAI.Balanced.TupleAlignment.alignedChildToPair line 103
  14. def OAI.Balanced.TupleAlignment.alignedChildOffsetsEquiv line 110
  15. abbrev OAI.Balanced.TupleAlignment.ChildOffsetsAt line 148
  16. def OAI.Balanced.TupleAlignment.childRotationEquiv line 151
  17. theorem OAI.Balanced.TupleAlignment.rotated_adjacent line 165
  18. theorem OAI.Balanced.TupleAlignment.tuplePosition_rotation line 171
  19. abbrev OAI.Balanced.TupleAlignment.AlignedChildOffsetsAt line 179
  20. def OAI.Balanced.TupleAlignment.alignedChildRotationEquiv line 185
  21. def OAI.Balanced.TupleAlignment.alignedChildOffsetsAtEquiv line 207
  22. instance OAI.Balanced.TupleAlignment.(instance at line 215) line 215
  23. instance OAI.Balanced.TupleAlignment.(instance at line 218) line 218
  24. theorem OAI.Balanced.TupleAlignment.card_childOffsets line 225
  25. theorem OAI.Balanced.TupleAlignment.card_alignedChildOffsets line 230
  26. theorem OAI.Balanced.TupleAlignment.alignedChildOffsets_probability line 237
  27. theorem OAI.Balanced.TupleAlignment.alignedChildOffsets_pmf_probability line 247
  28. theorem OAI.Balanced.TupleAlignment.card_childOffsetsAt line 258
  29. theorem OAI.Balanced.TupleAlignment.card_alignedChildOffsetsAt line 262
  30. theorem OAI.Balanced.TupleAlignment.alignedChildOffsetsAt_pmf_probability line 269
  31. theorem OAI.Balanced.TupleAlignment.alignedChildOffsetsAt_supported line 283
  32. theorem OAI.Balanced.TupleAlignment.alignedChildOffsetsAt_conditional_law line 292