OAI/NumberTheory/Jacobsthal/Paths/RawPhysicalHit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawHitRecord line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawHitRecord_measurable line 19
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawWord_last_physical line 26
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstHit_ae_physical line 36
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawFirstHit_ae_input_window line 49
6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawPhysicalHitEvent line 54
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawPhysicalHitEvent_measurable line 57
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawRegFirstHit_ae_physical line 61
9. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHitRecord line 72
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHitRecord_measurable line 75
11. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenPhysicalHitEvent line 80
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenPhysicalHitEvent_measurable line 83
13. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_ae_physical line 87