OAI/Probability/SignedSweeps/ReverseEncounters.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.labelNetwork_eq_none_iff line 14
2. lemma OAI.SignedSweeps.labelNetwork_eq_some_iff line 19
3. lemma OAI.SignedSweeps.mem_networkInitialSubsets line 31
4. def OAI.SignedSweeps.labelLocation line 41
5. def OAI.SignedSweeps.labelOccupancy line 44
6. lemma OAI.SignedSweeps.labelLocation_injective_sampled line 48
7. lemma OAI.SignedSweeps.labelOccupancy_eq_sampleSubset line 58
8. def OAI.SignedSweeps.reverseNetworkState line 91
9. lemma OAI.SignedSweeps.reverseNetworkState_eq_endpointPath line 96
10. lemma OAI.SignedSweeps.same_switch_eq_or_flip line 104
11. lemma OAI.SignedSweeps.endpointEncounter_maps_to_network line 113
12. lemma OAI.SignedSweeps.NoIsolatedVertex_image line 129
13. lemma OAI.SignedSweeps.reverse_endpoint_noIsolates_implies_network line 138