OAI/Probability/SwitchChain/PairSwapFlip.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PairFiber.reverse_fourVertexProposal line 11
2. theorem OAI.Problem315.PairFiber.valid_fourVertex_iff_left_membership line 22
3. theorem OAI.Problem315.PairFiber.state_eq_bidirectional_of_key_leftSet_swap line 38
4. theorem OAI.Problem315.PairFiber.assignmentRelabel_swap_eq_bidirectional line 90
5. theorem OAI.Problem315.PairFiber.fourDistinct_of_singleton_labels line 124
6. theorem OAI.Problem315.PairFiber.singleton_labels_of_valid_fourVertex line 132
7. theorem OAI.Problem315.PairFiber.bidirectional_eq_self_of_not_singleton line 144
8. theorem OAI.Problem315.PairFiber.fourVertexProposal_exchange_pairs line 161