OAI/Combinatorics/KMedianRecovery/Branching/CopyGround.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Completion.CopyGround.part line 9
  2. def OAI.MetricKMedianRecovery.Completion.CopyGround.location line 10
  3. lemma OAI.MetricKMedianRecovery.Completion.CopyGround.location_mem line 12
  4. def OAI.MetricKMedianRecovery.Completion.CopyGround.embed line 18
  5. lemma OAI.MetricKMedianRecovery.Completion.CopyGround.part_embed line 19
  6. lemma OAI.MetricKMedianRecovery.Completion.CopyGround.mod_embed line 21
  7. lemma OAI.MetricKMedianRecovery.Completion.CopyGround.location_embed line 23
  8. def OAI.MetricKMedianRecovery.Completion.CopyGround.origin line 26
  9. lemma OAI.MetricKMedianRecovery.Completion.CopyGround.part_origin line 28
  10. lemma OAI.MetricKMedianRecovery.Completion.CopyGround.part_surjective line 30
  11. lemma OAI.MetricKMedianRecovery.Completion.CopyGround.lift_feasible line 32
  12. lemma OAI.MetricKMedianRecovery.Completion.surrogate_image line 39
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.pack line 50
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.ball line 52
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.ball_computes line 54
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.entry line 56
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.entry_computes line 59
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.columns line 62
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.columns_computes line 63
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.row line 65
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.row_computes line 67
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.indices line 70
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.indices_computes line 71
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.locations line 72
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.locations_computes line 73
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.partRow line 76
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.partRow_computes line 77
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.parts line 80
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.parts_computes line 81
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.origin line 84
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.origin_computes line 86
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.origins line 92
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.origins_computes line 93
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.head_set line 96
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.contains_set line 109
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.ball_pack line 117
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.columns_pack line 120
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.indices_pack line 123
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.entry_pack line 126
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.row_pack line 134
  41. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.encoded_ofFn_flatten line 138
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.equiv_mk line 142
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.locations_pack line 146
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.parts_pack line 153
  45. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCopyTables.origins_pack line 167