OAI/Combinatorics/KMedianRecovery/Branching/CategoricalChoice.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.OrderedMaximum.cast_ofList line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.elements line 16
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.mem_elements line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.rule line 18
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.bagTest line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.bagTest_computes line 23
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.bagWords line 26
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.bagWords_computes line 28
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.bagTest_pack line 31
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.bagWords_pack line 36
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.choose line 50
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.choose_computes line 52
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.choose_pack line 54
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.choices line 67
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.choices_computes line 70
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.choices_pack line 73
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.stepContext line 90
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.stateBits line 92
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.stepScore line 93
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.stepScore_computes line 95
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.nextTable line 99
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.nextTable_computes line 102
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.step line 107
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.step_computes line 111
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.stepScore_pack line 118
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.nextTable_pack line 123
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.step_pack line 135