OAI/Combinatorics/KMedianRecovery/Recovery/Leaf.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.PhaseLeafGeometry.Data.leaf line 11
  2. lemma OAI.MetricKMedianRecovery.PhaseLeafGeometry.double_pool_eq line 32
  3. def OAI.MetricKMedianRecovery.PhaseLeafGeometry.Data.allocate line 46
  4. theorem OAI.MetricKMedianRecovery.PhaseGeometricMerge.leaf_success line 67
  5. def OAI.MetricKMedianRecovery.PhaseGeometricMerge.leaf_bracket line 85
  6. def OAI.MetricKMedianRecovery.PhaseGeometricMerge.Claim line 114
  7. lemma OAI.MetricKMedianRecovery.PhaseGeometricMerge.diameter_map line 123
  8. theorem OAI.MetricKMedianRecovery.PhaseGeometricMerge.outcome_solved line 133
  9. theorem OAI.MetricKMedianRecovery.PhaseGeometricMerge.crossing_solved line 177
  10. theorem OAI.MetricKMedianRecovery.PhaseGeometricMerge.solve line 217