OAI/Combinatorics/KMedianRecovery/Recovery/ReverseRow.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Ellipsoid.reverseRow line 10
  2. lemma OAI.MetricKMedianRecovery.Ellipsoid.reverseRow_holds line 12
  3. def OAI.MetricKMedianRecovery.Ellipsoid.faceRows line 16
  4. def OAI.MetricKMedianRecovery.Ellipsoid.Face line 19
  5. lemma OAI.MetricKMedianRecovery.Ellipsoid.faceRows_holds line 23
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.decide_face line 42
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.Face.of_subset line 50
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.Face.cons line 54
  9. def OAI.MetricKMedianRecovery.Ellipsoid.selectFace line 63
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.selectFace_spec line 71
  11. lemma OAI.MetricKMedianRecovery.Ellipsoid.selectFace_length line 97