OAI/Combinatorics/KMedianRecovery/Encoding/RationalLeaves.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.RationalLeaves.Label line 10
  2. def OAI.MetricKMedianRecovery.RationalLeaves.root line 12
  3. def OAI.MetricKMedianRecovery.RationalLeaves.height line 13
  4. def OAI.MetricKMedianRecovery.RationalLeaves.metric line 15
  5. def OAI.MetricKMedianRecovery.RationalLeaves.original line 22
  6. def OAI.MetricKMedianRecovery.RationalLeaves.leaf line 23
  7. def OAI.MetricKMedianRecovery.RationalLeaves.parent line 25
  8. def OAI.MetricKMedianRecovery.RationalLeaves.rows line 27
  9. lemma OAI.MetricKMedianRecovery.RationalLeaves.original_dist line 32
  10. lemma OAI.MetricKMedianRecovery.RationalLeaves.leaf_dist line 35
  11. lemma OAI.MetricKMedianRecovery.RationalLeaves.rows_spec line 39
  12. def OAI.MetricKMedianRecovery.RationalLeaves.Before line 55
  13. lemma OAI.MetricKMedianRecovery.RationalLeaves.fresh line 59
  14. lemma OAI.MetricKMedianRecovery.RationalLeaves.Before.mono line 68
  15. lemma OAI.MetricKMedianRecovery.RationalLeaves.Before.subset line 72
  16. def OAI.MetricKMedianRecovery.RationalLeaves.copy line 75
  17. lemma OAI.MetricKMedianRecovery.RationalLeaves.copy_dist line 79
  18. lemma OAI.MetricKMedianRecovery.RationalLeaves.pool_before line 85
  19. lemma OAI.MetricKMedianRecovery.RationalLeaves.singleton_before line 97
  20. def OAI.MetricKMedianRecovery.RationalLeaves.shorten line 106
  21. lemma OAI.MetricKMedianRecovery.RationalLeaves.shorten_injective line 110
  22. lemma OAI.MetricKMedianRecovery.RationalLeaves.shorten_original line 114
  23. lemma OAI.MetricKMedianRecovery.RationalLeaves.shorten_old line 118
  24. lemma OAI.MetricKMedianRecovery.RationalLeaves.shorten_dist line 124