OAI/Probability/FreeIsing/Trees/PathSideBranches.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PathSideBranches.cone line 9
  2. def OAI.Problem367.PathSideBranches.sideColor line 12
  3. theorem OAI.Problem367.PathSideBranches.sideColor_ne_incoming line 17
  4. theorem OAI.Problem367.PathSideBranches.sideColor_ne_outgoing line 22
  5. theorem OAI.Problem367.PathSideBranches.take_target_ne_nil line 31
  6. def OAI.Problem367.PathSideBranches.sideVertex line 39
  7. theorem OAI.Problem367.PathSideBranches.sideVertex_val line 48
  8. theorem OAI.Problem367.PathSideBranches.sideVertex_length line 52
  9. theorem OAI.Problem367.PathSideBranches.parent_sideVertex line 57
  10. theorem OAI.Problem367.PathSideBranches.sideVertex_adj line 63
  11. theorem OAI.Problem367.PathSideBranches.not_prefix_wrong_color line 68
  12. theorem OAI.Problem367.PathSideBranches.sideVertex_not_prefix line 84
  13. theorem OAI.Problem367.PathSideBranches.cone_mono line 93
  14. theorem OAI.Problem367.PathSideBranches.path_vertex_not_mem_sideCone line 96
  15. theorem OAI.Problem367.PathSideBranches.sideCone_disjoint_later_forward line 102
  16. theorem OAI.Problem367.PathSideBranches.sideCone_subset_forward line 117
  17. theorem OAI.Problem367.PathSideBranches.sideCones_pairwise_disjoint line 122
  18. theorem OAI.Problem367.PathSideBranches.cone_infinite line 132
  19. theorem OAI.Problem367.PathSideBranches.sideCone_infinite line 142
  20. theorem OAI.Problem367.PathSideBranches.edge_leaving_cone line 150
  21. theorem OAI.Problem367.PathSideBranches.sideCone_boundary line 168
  22. theorem OAI.Problem367.PathSideBranches.reachable_in_cone line 176
  23. theorem OAI.Problem367.PathSideBranches.parent_not_mem_cone line 208
  24. theorem OAI.Problem367.PathSideBranches.mem_cone_iff_reachable_avoiding_parent line 216