OAI/Computability/PerfectCompleteness/Foundations/SlotProjectedExperiment.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SlotProjectedExperiment.selectSlot line 16
  2. def OAI.PerfectCompleteness.SlotProjectedExperiment.selectProjection line 20
  3. def OAI.PerfectCompleteness.SlotProjectedExperiment.flaggedSlot line 26
  4. def OAI.PerfectCompleteness.SlotProjectedExperiment.flaggedProjection line 30
  5. def OAI.PerfectCompleteness.SlotProjectedExperiment.mixedInside line 37
  6. def OAI.PerfectCompleteness.SlotProjectedExperiment.insideProjection line 43
  7. abbrev OAI.PerfectCompleteness.SlotProjectedExperiment.Inner line 49
  8. abbrev OAI.PerfectCompleteness.SlotProjectedExperiment.innerLaw line 52
  9. def OAI.PerfectCompleteness.SlotProjectedExperiment.upperPath line 60
  10. abbrev OAI.PerfectCompleteness.SlotProjectedExperiment.lowerPath line 62
  11. def OAI.PerfectCompleteness.SlotProjectedExperiment.stoppedPath line 65
  12. def OAI.PerfectCompleteness.SlotProjectedExperiment.upper line 68
  13. def OAI.PerfectCompleteness.SlotProjectedExperiment.lower line 70
  14. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.upper_height line 73
  15. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.lower_height line 76
  16. def OAI.PerfectCompleteness.SlotProjectedExperiment.cut line 81
  17. def OAI.PerfectCompleteness.SlotProjectedExperiment.direction line 86
  18. def OAI.PerfectCompleteness.SlotProjectedExperiment.inside line 94
  19. def OAI.PerfectCompleteness.SlotProjectedExperiment.projectedSlots line 98
  20. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.fill_inside line 103
  21. def OAI.PerfectCompleteness.SlotProjectedExperiment.projection line 108
  22. abbrev OAI.PerfectCompleteness.SlotProjectedExperiment.Sample line 118
  23. abbrev OAI.PerfectCompleteness.SlotProjectedExperiment.experiment line 126
  24. def OAI.PerfectCompleteness.SlotProjectedExperiment.family line 133
  25. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.mark_eq line 140
  26. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.tree_sources line 160
  27. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.mixedInside_source line 172
  28. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.projection_family_heq line 184
  29. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.mpr_heq line 195
  30. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.flagged_occurrence_heq line 200
  31. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.child_projection_as_flagged line 207
  32. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.insideProjection_source line 216
  33. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.projectedSlots_source line 237
  34. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.filled_projection_heq line 250
  35. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.projection_source line 268
  36. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.tagged_projection_heq line 286
  37. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.projected_experiment_heq line 298
  38. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.experiment_source line 317
  39. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.projection_data_congr line 327
  40. theorem OAI.PerfectCompleteness.SlotProjectedExperiment.mark_source line 342