OAI/Probability/SwitchChain/PairOrbit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.PairOrbit.membershipColor line 11
2. theorem OAI.Problem315.PairOrbit.color_filter line 14
3. theorem OAI.Problem315.PairOrbit.membershipColor_fiber_card line 21
4. theorem OAI.Problem315.PairOrbit.exists_perm_membership line 47
5. theorem OAI.Problem315.PairOrbit.image_eq_of_membership line 68
6. theorem OAI.Problem315.PairOrbit.exists_perm_image line 82
7. theorem OAI.Problem315.PairOrbit.invariant_kernel_eq_of_card line 90
8. theorem OAI.Problem315.PairOrbit.invariant_pair_kernel_eq_of_intersection line 99
9. theorem OAI.Problem315.PairOrbit.gram_invariant line 109
10. theorem OAI.Problem315.PairOrbit.gram_eq_of_intersection line 120