OAI/Combinatorics/KMedianRecovery/Recovery/CanonicalParents.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.RationalLeaves.parent_original line 11
  2. lemma OAI.MetricKMedianRecovery.RationalLeaves.parent_leaf line 13
  3. lemma OAI.MetricKMedianRecovery.RationalLeaves.parent_copy line 15
  4. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Rooted line 20
  5. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.rooted_empty line 22
  6. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.correction_parent line 23
  7. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.rooted_mapFree line 27
  8. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.rooted_pool line 32
  9. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.rooted_banks line 40
  10. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.rooted_insert line 42
  11. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Outcome.Rooted line 49
  12. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.resolve_rooted line 52
  13. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.step_rooted line 69
  14. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.run_rooted line 83
  15. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.StartOutput.Rooted line 95
  16. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.start_rooted line 98
  17. def OAI.MetricKMedianRecovery.RationalLeaves.project line 116
  18. lemma OAI.MetricKMedianRecovery.RationalLeaves.project_nonempty line 118
  19. lemma OAI.MetricKMedianRecovery.RationalLeaves.project_card line 120
  20. lemma OAI.MetricKMedianRecovery.RationalLeaves.parent_distance line 122
  21. lemma OAI.MetricKMedianRecovery.RationalLeaves.project_distance line 130
  22. lemma OAI.MetricKMedianRecovery.RationalLeaves.project_subset line 139
  23. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Output.project line 153
  24. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Output.normal_certificate line 155