OAI/Combinatorics/MatchingCount/Sampling/Components.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.components line 14
  2. lemma OAI.MatchingFPRAS.Transport.mem_components line 18
  3. lemma OAI.MatchingFPRAS.Transport.componentEdges_subset line 24
  4. lemma OAI.MatchingFPRAS.Transport.componentEdges_self line 29
  5. lemma OAI.MatchingFPRAS.Transport.componentEdges_eq line 34
  6. lemma OAI.MatchingFPRAS.Transport.component_nonempty line 41
  7. lemma OAI.MatchingFPRAS.Transport.component_subset line 45
  8. lemma OAI.MatchingFPRAS.Transport.component_eq_of_shares line 49
  9. lemma OAI.MatchingFPRAS.Transport.components_pairwise_disjoint line 58
  10. lemma OAI.MatchingFPRAS.Transport.components_cover line 70
  11. lemma OAI.MatchingFPRAS.Transport.component_exists_vertex line 81
  12. def OAI.MatchingFPRAS.Transport.componentVertex line 88
  13. lemma OAI.MatchingFPRAS.Transport.componentVertex_injective line 92
  14. lemma OAI.MatchingFPRAS.Transport.components_card_le line 103
  15. lemma OAI.MatchingFPRAS.Transport.component_exchange_compatible line 108
  16. def OAI.MatchingFPRAS.Transport.IndexedCycle.edgeSet line 119
  17. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.mem_edgeSet line 121
  18. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt_mem_edgeSet line 129
  19. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeSet_subset line 133
  20. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.previous_indices line 139
  21. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edge_incident_cycle_mem line 151
  22. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeSet_closed line 181
  23. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeSet_eq_component line 193
  24. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeSet_mem_components line 210
  25. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.inter_edgeSet_parity line 216
  26. lemma OAI.MatchingFPRAS.Transport.CellPaths.mem_assemble_iff line 245
  27. lemma OAI.MatchingFPRAS.Transport.CellPaths.assemble_update line 257
  28. def OAI.MatchingFPRAS.Transport.CellPaths.conversionPieces line 274
  29. def OAI.MatchingFPRAS.Transport.CellPaths.converted line 277
  30. lemma OAI.MatchingFPRAS.Transport.CellPaths.conversion_pieces_matching line 280
  31. lemma OAI.MatchingFPRAS.Transport.CellPaths.converted_matching line 289
  32. lemma OAI.MatchingFPRAS.Transport.CellPaths.converted_empty line 294
  33. lemma OAI.MatchingFPRAS.Transport.CellPaths.conversion_pieces_insert line 298
  34. lemma OAI.MatchingFPRAS.Transport.CellPaths.converted_insert line 306
  35. lemma OAI.MatchingFPRAS.Transport.CellPaths.converted_singleton line 318
  36. lemma OAI.MatchingFPRAS.Transport.CellPaths.converted_pair line 324
  37. lemma OAI.MatchingFPRAS.Transport.CellPaths.double_conversion line 336
  38. def OAI.MatchingFPRAS.Transport.CellPaths.canonicalGain line 346
  39. def OAI.MatchingFPRAS.Transport.CellPaths.contextError line 349
  40. lemma OAI.MatchingFPRAS.Transport.CellPaths.opposite_pair_identity line 354
  41. theorem OAI.MatchingFPRAS.Transport.CellPaths.single_cell_identity line 363