OAI/Combinatorics/KMedianRecovery/Recovery/KindRows.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.EffectiveOpenability.kindRows line 12
2. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.mem_kindRows line 19
3. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.length_kindRows line 24
4. def OAI.MetricKMedianRecovery.EffectiveOpenability.variableEnum line 30
5. def OAI.MetricKMedianRecovery.EffectiveOpenability.subtypeList line 36
6. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.mem_subtypeList line 39
7. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.subtypeList_length line 42
8. def OAI.MetricKMedianRecovery.EffectiveOpenability.exactOpening line 49
9. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.exactOpening_sound line 54
10. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.exactOpening_complete line 67
11. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.exactOpening_none_iff line 76
12. lemma OAI.MetricKMedianRecovery.Ellipsoid.scalar_cut_bound line 97
13. lemma OAI.MetricKMedianRecovery.Ellipsoid.unit_ball_cut line 116
14. lemma OAI.MetricKMedianRecovery.Ellipsoid.determinant_growth line 136