OAI/Combinatorics/KMedianRecovery/Recovery/FacePoint.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Ellipsoid.finalFace_injective line 10
2. lemma OAI.MetricKMedianRecovery.Ellipsoid.finalFace_rat_injective line 25
3. def OAI.MetricKMedianRecovery.Ellipsoid.facePoint line 38
4. theorem OAI.MetricKMedianRecovery.Ellipsoid.facePoint_correct line 45
5. def OAI.MetricKMedianRecovery.Ellipsoid.exactSolve line 74
6. theorem OAI.MetricKMedianRecovery.Ellipsoid.exactSolve_some line 77
7. theorem OAI.MetricKMedianRecovery.Ellipsoid.exactSolve_complete line 94
8. theorem OAI.MetricKMedianRecovery.OpenabilityLinearization.normalize_bounded line 104
9. theorem OAI.MetricKMedianRecovery.OpenabilityLinearization.openable_iff_bounded line 170