OAI/Probability/FreeIsing/Trees/OpenClusterGeometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.OpenCluster.openAdj line 15
  2. def OAI.Problem367.OpenCluster.downwardOpen line 18
  3. lemma OAI.Problem367.OpenCluster.openAdj_symm line 22
  4. lemma OAI.Problem367.OpenCluster.reachable_symm line 33
  5. lemma OAI.Problem367.OpenCluster.open_of_crossing_prefix line 40
  6. lemma OAI.Problem367.OpenCluster.open_of_reachable_crossing_prefix line 57
  7. lemma OAI.Problem367.OpenCluster.downwardOpen_refl line 67
  8. lemma OAI.Problem367.OpenCluster.downwardOpen_of_reachable line 73
  9. lemma OAI.Problem367.OpenCluster.prefix_of_reachable_min line 86
  10. lemma OAI.Problem367.OpenCluster.exists_min_reachable line 98
  11. lemma OAI.Problem367.OpenCluster.reachable_subset_downwardOpen line 111
  12. theorem OAI.Problem367.OpenCluster.finite_reachable_of_finite_downwardOpen line 123
  13. lemma OAI.Problem367.OpenCluster.reachable_of_downwardOpen line 129
  14. theorem OAI.Problem367.OpenCluster.exists_reachable_eq_downwardOpen line 153
  15. theorem OAI.Problem367.OpenCluster.openAdj_incoming_iff line 162
  16. theorem OAI.Problem367.OpenCluster.finite_reachable_of_finite_incoming line 187