OAI/Combinatorics/KMedianRecovery/Recovery/StoredForms.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalLinearFeasibility.storedForms line 11
  2. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.storedForms_sound line 16
  3. lemma OAI.MetricKMedianRecovery.RationalLinearFeasibility.storedForms_complete line 24
  4. def OAI.MetricKMedianRecovery.EffectiveOpenability.storedOpening line 39
  5. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.storedOpening_witness line 45
  6. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.storedOpening_sound line 58
  7. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.storedOpening_complete line 68
  8. lemma OAI.MetricKMedianRecovery.EffectiveOpenability.storedOpening_none_iff line 92
  9. structure OAI.MetricKMedianRecovery.RationalPhase.State line 113
  10. structure OAI.MetricKMedianRecovery.RationalPhase.Event line 118
  11. def OAI.MetricKMedianRecovery.RationalPhase.State.real line 122
  12. def OAI.MetricKMedianRecovery.RationalPhase.update line 125
  13. lemma OAI.MetricKMedianRecovery.RationalPhase.update_get line 130
  14. lemma OAI.MetricKMedianRecovery.RationalPhase.update_real line 136
  15. def OAI.MetricKMedianRecovery.RationalPhase.first line 156
  16. lemma OAI.MetricKMedianRecovery.RationalPhase.first_some line 166
  17. lemma OAI.MetricKMedianRecovery.RationalPhase.first_none_iff line 187
  18. lemma OAI.MetricKMedianRecovery.RationalPhase.first_plain line 222
  19. lemma OAI.MetricKMedianRecovery.RationalPhase.first_none_maximal line 245
  20. def OAI.MetricKMedianRecovery.RationalPhase.finish line 257