OAI/Combinatorics/MatchingCount/Graphs/SumLiftMate.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.Switching.sumLiftMate line 14
2. lemma OAI.MatchingFPRAS.Switching.sumLiftMate_inl line 17
3. lemma OAI.MatchingFPRAS.Switching.sumLiftMate_inr line 20
4. def OAI.MatchingFPRAS.Switching.sumRetractMate line 23
5. lemma OAI.MatchingFPRAS.Switching.sumRetractMate_inl line 38
6. lemma OAI.MatchingFPRAS.Switching.sumLift_retract line 47
7. lemma OAI.MatchingFPRAS.Switching.sumLift_holes line 54
8. lemma OAI.MatchingFPRAS.Switching.internal_fixed_of_terminal_holes line 65
9. lemma OAI.MatchingFPRAS.Switching.sumLift_weight line 70
10. theorem OAI.MatchingFPRAS.Switching.pairingCapacity_sum_inl line 77
11. theorem OAI.MatchingFPRAS.Switching.ChargeTrace.capacity_bound_decidable line 111
12. lemma OAI.MatchingFPRAS.Switching.ChargeTrace.factor_nonneg line 125
13. abbrev OAI.MatchingFPRAS.Subdivision.Selection line 138
14. def OAI.MatchingFPRAS.Subdivision.Valid line 140
15. def OAI.MatchingFPRAS.Subdivision.alternating line 144
16. theorem OAI.MatchingFPRAS.Subdivision.alternating_zero line 146
17. theorem OAI.MatchingFPRAS.Subdivision.alternating_succ line 149
18. theorem OAI.MatchingFPRAS.Subdivision.alternating_add_two line 158
19. lemma OAI.MatchingFPRAS.Subdivision.bool_ne_iff_eq_not line 163
20. theorem OAI.MatchingFPRAS.Subdivision.intact_iff line 166
21. theorem OAI.MatchingFPRAS.Subdivision.intact_terminals line 188
22. theorem OAI.MatchingFPRAS.Subdivision.alternating_valid line 193
23. theorem OAI.MatchingFPRAS.Subdivision.alternating_not line 199
24. def OAI.MatchingFPRAS.Subdivision.wordWeight line 204
25. theorem OAI.MatchingFPRAS.Subdivision.wordWeight_nil line 208
26. theorem OAI.MatchingFPRAS.Subdivision.wordWeight_pair line 210
27. def OAI.MatchingFPRAS.Subdivision.duplicate line 214
28. theorem OAI.MatchingFPRAS.Subdivision.duplicate_nil line 216
29. theorem OAI.MatchingFPRAS.Subdivision.duplicate_cons line 218
30. theorem OAI.MatchingFPRAS.Subdivision.duplicate_length line 221
31. theorem OAI.MatchingFPRAS.Subdivision.paired_prefix_weight line 227
32. theorem OAI.MatchingFPRAS.Subdivision.profile_weight line 233
33. theorem OAI.MatchingFPRAS.Subdivision.wordWeight_ofFn line 243
34. def OAI.MatchingFPRAS.Subdivision.selectedWeight line 256
35. theorem OAI.MatchingFPRAS.Subdivision.intact_weight line 259
36. def OAI.MatchingFPRAS.Subdivision.LogicalPerfect line 269
37. def OAI.MatchingFPRAS.Subdivision.FamilyPerfect line 272
38. theorem OAI.MatchingFPRAS.Subdivision.family_iff line 278
39. def OAI.MatchingFPRAS.Subdivision.familyEquiv line 293
40. def OAI.MatchingFPRAS.Subdivision.logicalPartition line 309
41. def OAI.MatchingFPRAS.Subdivision.realPartition line 315
42. theorem OAI.MatchingFPRAS.Subdivision.family_weight line 323
43. theorem OAI.MatchingFPRAS.Subdivision.real_partition_identity line 336