OAI/Computability/PerfectCompleteness/Repetition/CleanRecordObservation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.CleanRecordObservation.Record line 19
2. abbrev OAI.PerfectCompleteness.CleanRecordObservation.Sample line 20
3. def OAI.PerfectCompleteness.CleanRecordObservation.observe line 22
4. theorem OAI.PerfectCompleteness.CleanRecordObservation.event_eq line 29
5. theorem OAI.PerfectCompleteness.CleanRecordObservation.event_observe line 38
6. def OAI.PerfectCompleteness.CleanRecordObservation.leftQuestions line 44
7. def OAI.PerfectCompleteness.CleanRecordObservation.rightQuestions line 50
8. theorem OAI.PerfectCompleteness.CleanRecordObservation.leftInside_eq line 56
9. theorem OAI.PerfectCompleteness.CleanRecordObservation.rightInside_eq line 73