OAI/Combinatorics/KMedianRecovery/Recovery/Ball.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Population.ball line 8
  2. lemma OAI.MetricKMedianRecovery.Population.ball_mono line 11
  3. lemma OAI.MetricKMedianRecovery.Population.ball_nonempty_at line 16
  4. def OAI.MetricKMedianRecovery.Population.candidate line 19
  5. def OAI.MetricKMedianRecovery.Population.radius line 22
  6. lemma OAI.MetricKMedianRecovery.Population.candidate_pos line 25
  7. lemma OAI.MetricKMedianRecovery.Population.radius_pos line 31
  8. lemma OAI.MetricKMedianRecovery.Population.candidate_feasible line 37
  9. lemma OAI.MetricKMedianRecovery.Population.radius_feasible line 53
  10. lemma OAI.MetricKMedianRecovery.Population.radius_minimal line 59
  11. lemma OAI.MetricKMedianRecovery.Population.radius_isLeast line 81
  12. lemma OAI.MetricKMedianRecovery.Population.sublevel_card line 89
  13. lemma OAI.MetricKMedianRecovery.Population.leader_radius_le line 131
  14. lemma OAI.MetricKMedianRecovery.Population.third_balls_disjoint line 171
  15. lemma OAI.MetricKMedianRecovery.Population.disjoint_population_budget line 194
  16. lemma OAI.MetricKMedianRecovery.Population.ceiling_index_budget line 237