OAI/Probability/SwitchChain/PairSwapInactive.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PairFiber.singleton_labels_of_valid_reverse_fourVertex line 11
2. theorem OAI.Problem315.PairFiber.not_valid_of_nonsingleton line 26
3. theorem OAI.Problem315.PairFiber.bidirectional_proposal_fix_of_nonsingleton line 39
4. theorem OAI.Problem315.PairFiber.nonsingleton_of_sameFiber line 51
5. theorem OAI.Problem315.PairFiber.bidirectional_proposal_fix_on_inactive_fiber line 59