OAI/Probability/SwitchChain/DisjointBlockGraph.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.DisjointBlock.Vertex line 10
  2. structure OAI.Problem315.DisjointBlock.Data line 12
  3. def OAI.Problem315.DisjointBlock.adjacency line 22
  4. def OAI.Problem315.DisjointBlock.graph line 33
  5. def OAI.Problem315.DisjointBlock.encode line 49
  6. theorem OAI.Problem315.DisjointBlock.graph_encode line 59
  7. theorem OAI.Problem315.DisjointBlock.encode_graph line 70
  8. def OAI.Problem315.DisjointBlock.graphEquiv line 80
  9. def OAI.Problem315.DisjointBlock.indicator line 86
  10. def OAI.Problem315.DisjointBlock.valence line 90
  11. theorem OAI.Problem315.DisjointBlock.valence_eq_degree line 93
  12. theorem OAI.Problem315.DisjointBlock.internal_indicator_sum line 102
  13. theorem OAI.Problem315.DisjointBlock.bool_indicator line 106
  14. theorem OAI.Problem315.DisjointBlock.valence_graph_A line 109
  15. theorem OAI.Problem315.DisjointBlock.valence_graph_B line 116
  16. theorem OAI.Problem315.DisjointBlock.valence_graph_outside line 123