OAI/Probability/SpanningForest/InducedCode.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.inducedCode line 8
  2. theorem OAI.Problem336.inducedCode_vertices line 12
  3. theorem OAI.Problem336.mem_inducedCode_edges line 15
  4. theorem OAI.Problem336.inducedCode_adj_symm line 24
  5. theorem OAI.Problem336.inducedCode_adj_ne line 28
  6. theorem OAI.Problem336.rawPair_mem_inducedCode_edges line 35
  7. theorem OAI.Problem336.subgraphAdj_inducedCode line 49
  8. theorem OAI.Problem336.inducedCode_isFiniteConnectedSubgraph line 54
  9. theorem OAI.Problem336.inducedCode_mono line 66
  10. theorem OAI.Problem336.inducedCode_isConnectedExhaustion line 74
  11. theorem OAI.Problem336.measurable_inducedCode line 89