OAI/Probability/FreeIsing/Trees/ConnectedHull.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ConnectedHull.root line 11
  2. def OAI.Problem367.ConnectedHull.takeVertex line 13
  3. theorem OAI.Problem367.ConnectedHull.prefix_zero line 16
  4. theorem OAI.Problem367.ConnectedHull.prefix_length line 20
  5. theorem OAI.Problem367.ConnectedHull.prefix_adj line 25
  6. def OAI.Problem367.ConnectedHull.vertices line 30
  7. def OAI.Problem367.ConnectedHull.hull line 34
  8. theorem OAI.Problem367.ConnectedHull.prefix_mem_hull line 38
  9. theorem OAI.Problem367.ConnectedHull.subset_hull line 46
  10. theorem OAI.Problem367.ConnectedHull.prefix_paths line 50
  11. theorem OAI.Problem367.ConnectedHull.hull_paths line 70
  12. theorem OAI.Problem367.ConnectedHull.connected_hull line 89
  13. theorem OAI.Problem367.exists_connectedFinset_superset line 98