OAI/Computability/MatchingCount/OddCutParity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryMatching.OddCutParity.OddSide line 11
2. instance OAI.BinaryMatching.OddCutParity.oddSideDecidable line 12
3. lemma OAI.BinaryMatching.OddCutParity.terminal_partition line 15
4. lemma OAI.BinaryMatching.OddCutParity.even_other line 19
5. lemma OAI.BinaryMatching.OddCutParity.odd_other line 25
6. lemma OAI.BinaryMatching.OddCutParity.odd_separates line 34
7. lemma OAI.BinaryMatching.OddCutParity.separate_cards line 44
8. lemma OAI.BinaryMatching.OddCutParity.split_odd line 50
9. def OAI.BinaryMatching.OddCutParity.contractMap line 59
10. lemma OAI.BinaryMatching.OddCutParity.lift_contract line 62
11. lemma OAI.BinaryMatching.OddCutParity.lift_card line 68
12. lemma OAI.BinaryMatching.OddCutParity.odd_lift_iff line 81
13. lemma OAI.BinaryMatching.OddCutParity.lift_of_subset line 88
14. lemma OAI.BinaryMatching.OddCutParity.cut_contract_subset line 93
15. lemma OAI.BinaryMatching.OddCutParity.odd_subset_iff line 98