OAI/Probability/FreeIsing/Trees/FiniteClusterSelector.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.FiniteCluster.IsMinimum line 13
  2. theorem OAI.Problem367.FiniteCluster.IsMinimum.unique line 16
  3. def OAI.Problem367.FiniteCluster.selector line 21
  4. theorem OAI.Problem367.FiniteCluster.selector_eq_of_minimum line 25
  5. theorem OAI.Problem367.FiniteCluster.selector_eq_self_of_not_exists line 32
  6. theorem OAI.Problem367.FiniteCluster.selector_eq_iff line 37
  7. theorem OAI.Problem367.FiniteCluster.exists_minimum_of_finite line 57
  8. theorem OAI.Problem367.FiniteCluster.selector_mem line 65
  9. theorem OAI.Problem367.FiniteCluster.selector_eq_of_same_cluster line 72
  10. theorem OAI.Problem367.FiniteCluster.selector_eq_of_related line 82
  11. theorem OAI.Problem367.FiniteCluster.selector_eq_iff_related line 90
  12. theorem OAI.Problem367.FiniteCluster.isMinimum_reindex line 102
  13. theorem OAI.Problem367.FiniteCluster.selector_reindex line 121
  14. theorem OAI.Problem367.FiniteCluster.measurableSet_isMinimum line 141
  15. theorem OAI.Problem367.FiniteCluster.measurable_selector line 152
  16. def OAI.Problem367.FiniteCluster.color line 175
  17. theorem OAI.Problem367.FiniteCluster.color_eq_of_related line 179
  18. theorem OAI.Problem367.FiniteCluster.color_reindex line 186
  19. theorem OAI.Problem367.FiniteCluster.measurable_color line 192
  20. theorem OAI.Problem367.FiniteCluster.ae_marker_ne line 206
  21. theorem OAI.Problem367.FiniteCluster.ae_marker_injective line 218
  22. theorem OAI.Problem367.FiniteCluster.ae_uniform_markers_injective line 235