OAI/Probability/SwitchChain/PairSwapInjectivity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PairFiber.exchange_endpoints_unique line 10
2. theorem OAI.Problem315.PairFiber.swap_eq_of_map_eq line 28
3. theorem OAI.Problem315.PairFiber.exists_oriented_swap_of_map_ne line 37
4. theorem OAI.Problem315.PairFiber.map_swap_injective_on_nontrivial line 49
5. theorem OAI.Problem315.PairFiber.map_swap_injOn line 57