OAI/Probability/FreeIsing/Trees/Parents.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.parentVertex line 7
  2. theorem OAI.Problem367.parentVertex_val line 10
  3. theorem OAI.Problem367.parentVertex_length line 13
  4. theorem OAI.Problem367.treeAdj_length line 17
  5. theorem OAI.Problem367.treeAdj_parent_of_length_lt line 23
  6. theorem OAI.Problem367.treeAdj_lower_unique line 31
  7. theorem OAI.Problem367.treeAdj_parentVertex line 37
  8. theorem OAI.Problem367.treeAdj_preserves_prefix line 41
  9. theorem OAI.Problem367.treeAdj_preserves_prefix_of_parent_not_mem line 59
  10. theorem OAI.Problem367.prefix_of_reachable_of_parent_not_mem line 74
  11. theorem OAI.Problem367.ConnectedFinset.parent_mem_of_ne_min line 85
  12. theorem OAI.Problem367.ConnectedFinset.ne_nil_of_ne_min line 94
  13. theorem OAI.Problem367.ConnectedFinset.min_prefix line 106
  14. theorem OAI.Problem367.ConnectedFinset.min_unique line 122
  15. theorem OAI.Problem367.ConnectedFinset.prefix_mem_of_min_length_le line 129