OAI/Computability/PerfectCompleteness/Foundations/RawOccurrenceOrderLemmas.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.RawOccurrenceOrder.signedOrder line 21
  2. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.signedOrder_length line 25
  3. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.signedOrder_nodup line 29
  4. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.mem_signedOrder line 33
  5. def OAI.PerfectCompleteness.RawOccurrenceOrder.rawOrder line 38
  6. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.mem_rawOrder line 45
  7. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.rawOrder_eq_map_sigma line 56
  8. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.rawOrder_nodup line 64
  9. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.rawOrder_length line 72
  10. def OAI.PerfectCompleteness.RawOccurrenceOrder.fiberBound line 80
  11. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.signed_card_le_fiberBound line 83
  12. theorem OAI.PerfectCompleteness.RawOccurrenceOrder.rawOrder_length_le line 90
  13. def OAI.PerfectCompleteness.SignedMultiplicity.weights line 123
  14. theorem OAI.PerfectCompleteness.SignedMultiplicity.weights_positive line 126
  15. theorem OAI.PerfectCompleteness.SignedMultiplicity.weights_total line 130
  16. def OAI.PerfectCompleteness.SignedMultiplicity.baseDenominator line 134
  17. def OAI.PerfectCompleteness.SignedMultiplicity.baseCopies line 137
  18. theorem OAI.PerfectCompleteness.SignedMultiplicity.baseDenominator_positive line 140
  19. theorem OAI.PerfectCompleteness.SignedMultiplicity.baseCopies_positive line 143
  20. theorem OAI.PerfectCompleteness.SignedMultiplicity.baseCopies_total line 148
  21. theorem OAI.PerfectCompleteness.SignedMultiplicity.baseCopies_ratio line 155
  22. def OAI.PerfectCompleteness.SignedMultiplicity.denominator line 162
  23. theorem OAI.PerfectCompleteness.SignedMultiplicity.denominator_positive line 165
  24. def OAI.PerfectCompleteness.SignedMultiplicity.rawCopies line 172
  25. theorem OAI.PerfectCompleteness.SignedMultiplicity.rawCopies_total line 176
  26. def OAI.PerfectCompleteness.SignedMultiplicity.completedCopies line 193
  27. theorem OAI.PerfectCompleteness.SignedMultiplicity.completedCopies_positive line 199
  28. theorem OAI.PerfectCompleteness.SignedMultiplicity.completedCopies_total line 204
  29. theorem OAI.PerfectCompleteness.SignedMultiplicity.completedCopies_polynomial_total line 217
  30. theorem OAI.PerfectCompleteness.SignedMultiplicity.completedCopies_conditional_ratio line 225
  31. theorem OAI.PerfectCompleteness.SignedMultiplicity.completedCopies_mass line 241