OAI/Combinatorics/CycleDecomposition/EndpointPartition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ErdosGallai.endpoint_partition_of_family line 18
  2. def OAI.ErdosGallai.PositiveSimplePath.mapIso line 45
  3. theorem OAI.ErdosGallai.endpoint_partition_mapIso line 49
  4. lemma OAI.ErdosGallai.SimplePathPiece.deletedInduced_map line 87
  5. lemma OAI.ErdosGallai.SimplePathPiece.deletedInduced_edges line 93
  6. def OAI.ErdosGallai.SimplePathPiece.deletedPositive line 104
  7. theorem OAI.ErdosGallai.SimplePathPiece.endpoint_partition_after_deletion line 114
  8. def OAI.ErdosGallai.evenAugmentationOldIso line 179
  9. theorem OAI.ErdosGallai.endpoint_partition_of_augmented_parts line 184
  10. theorem OAI.ErdosGallai.lovasz_path_cycle_partition line 247
  11. theorem OAI.ErdosGallai.lovasz_theorem line 258
  12. theorem OAI.ErdosGallai.endpoint_path_partition line 261
  13. theorem OAI.ErdosGallai.endpoint_theorem line 265