OAI/Probability/FreeIsing/Trees/ClusterComponentCount.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ClusterComponentCount.openAdj line 12
  2. lemma OAI.Problem367.ClusterComponentCount.openAdj_symm line 16
  3. lemma OAI.Problem367.ClusterComponentCount.openAdj_treeAdj line 19
  4. def OAI.Problem367.ClusterComponentCount.openRoot line 27
  5. lemma OAI.Problem367.ClusterComponentCount.openRoot_of_nil line 36
  6. lemma OAI.Problem367.ClusterComponentCount.openRoot_of_closed line 40
  7. lemma OAI.Problem367.ClusterComponentCount.openRoot_of_open line 45
  8. lemma OAI.Problem367.ClusterComponentCount.openRoot_prefix line 50
  9. lemma OAI.Problem367.ClusterComponentCount.openRoot_length_le line 65
  10. lemma OAI.Problem367.ClusterComponentCount.openRoot_stopped line 68
  11. lemma OAI.Problem367.ClusterComponentCount.openRoot_idempotent line 84
  12. lemma OAI.Problem367.ClusterComponentCount.openRoot_eq_of_openAdj line 90
  13. lemma OAI.Problem367.ClusterComponentCount.openRoot_eq_of_connected line 96
  14. lemma OAI.Problem367.ClusterComponentCount.connected_openRoot line 102
  15. lemma OAI.Problem367.ClusterComponentCount.connected_symm line 118
  16. lemma OAI.Problem367.ClusterComponentCount.connected_of_openRoot_eq line 125
  17. lemma OAI.Problem367.ClusterComponentCount.connected_iff_openRoot_eq line 132
  18. lemma OAI.Problem367.ClusterComponentCount.openRoot_mem_or_eq line 136
  19. lemma OAI.Problem367.ClusterComponentCount.image_openRoot line 159
  20. lemma OAI.Problem367.ClusterComponentCount.openRoot_not_mem_closed line 182
  21. def OAI.Problem367.ClusterComponentCount.openEdges line 193
  22. lemma OAI.Problem367.ClusterComponentCount.image_openEdges_snd line 197
  23. theorem OAI.Problem367.ClusterComponentCount.card_image_openRoot line 212
  24. lemma OAI.Problem367.ClusterComponentCount.card_image_eq_of_same_fibers line 231
  25. theorem OAI.Problem367.ClusterComponentCount.card_image_componentLabel line 260
  26. theorem OAI.Problem367.ClusterComponentCount.connected_iff_internal line 272
  27. lemma OAI.Problem367.ClusterComponentCount.openAdj_iff_mem_openEdges line 279
  28. theorem OAI.Problem367.ClusterComponentCount.compatible_iff_component_constant line 312
  29. theorem OAI.Problem367.ClusterComponentCount.compatible_iff_label_constant line 337
  30. def OAI.Problem367.ClusterComponentCount.edgeMask line 350
  31. lemma OAI.Problem367.ClusterComponentCount.openAdj_edgeMask_iff line 353
  32. lemma OAI.Problem367.ClusterComponentCount.connected_edgeMask_iff line 382
  33. lemma OAI.Problem367.ClusterComponentCount.openEdges_edgeMask line 391
  34. theorem OAI.Problem367.ClusterComponentCount.card_image_of_relation line 401