OAI/Combinatorics/BalancedRyser/Local/TupleAlignment.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.TupleAlignment.lineEvalEquiv line 10
  2. theorem OAI.Balanced.TupleAlignment.lineEvalEquiv_apply line 47
  3. theorem OAI.Balanced.TupleAlignment.lineEvalEquiv_symm_apply line 50
  4. def OAI.Balanced.TupleAlignment.offsetPairsEquiv line 53
  5. def OAI.Balanced.TupleAlignment.tuplePositionEquiv line 64
  6. theorem OAI.Balanced.TupleAlignment.tuplePositionEquiv_apply line 70
  7. def OAI.Balanced.TupleAlignment.linePointEquiv line 77
  8. def OAI.Balanced.TupleAlignment.alignedOffsetsEquiv line 97
  9. theorem OAI.Balanced.TupleAlignment.aligned_injective_iff line 106
  10. def OAI.Balanced.TupleAlignment.alignedDistinctOffsetsEquiv line 125
  11. def OAI.Balanced.TupleAlignment.sameLineOffsetsEquiv line 135
  12. def OAI.Balanced.TupleAlignment.successfulOffsetsEquiv line 154
  13. theorem OAI.Balanced.TupleAlignment.uniform_map_equiv line 176
  14. theorem OAI.Balanced.TupleAlignment.card_alignedOffsets line 187
  15. theorem OAI.Balanced.TupleAlignment.card_alignedDistinctOffsets line 195
  16. theorem OAI.Balanced.TupleAlignment.card_sameLineOffsets line 205
  17. theorem OAI.Balanced.TupleAlignment.card_successfulOffsets line 215
  18. theorem OAI.Balanced.TupleAlignment.alignedOffsets_probability line 225
  19. theorem OAI.Balanced.TupleAlignment.tuplePosition_uniform line 237
  20. theorem OAI.Balanced.TupleAlignment.alignedOffsets_outer_probability line 243