OAI/Combinatorics/KMedianRecovery/Recovery/EllipsoidForms.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.ellipsoidForms line 10
2. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.ellipsoidForms_sound line 15
3. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.ellipsoidForms_complete line 23
4. def OAI.MetricKMedianRecovery.EffectiveOpenability.ellipsoidOpening line 38
5. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.ellipsoidOpening_witness line 44
6. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.ellipsoidOpening_sound line 57
7. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.ellipsoidOpening_complete line 67
8. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.ellipsoidOpening_none_iff line 91