OAI/Combinatorics/CycleDecomposition/DepthFirstSearch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ErdosGallai.Scale.DFSState line 19
  2. lemma OAI.ErdosGallai.Scale.DFSState.card_eq line 34
  3. lemma OAI.ErdosGallai.Scale.DFSState.restart line 43
  4. lemma OAI.ErdosGallai.Scale.DFSState.push line 59
  5. lemma OAI.ErdosGallai.Scale.DFSState.pop line 90
  6. lemma OAI.ErdosGallai.Scale.DFSState.reaches_balance line 112
  7. theorem OAI.ErdosGallai.Scale.exists_balanced_dfs_state line 137
  8. def OAI.ErdosGallai.Scale.externalNeighbors line 149
  9. def OAI.ErdosGallai.Scale.VertexExpansion line 152
  10. lemma OAI.ErdosGallai.Scale.DFSState.external_subset line 156
  11. theorem OAI.ErdosGallai.Scale.exists_long_stack line 167