OAI/Probability/FreeIsing/Estimates/FiniteComponentGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.rootComponentFinset line 10
  2. def OAI.Problem367.rootComplementFinset line 15
  3. theorem OAI.Problem367.mem_rootComponentFinset line 20
  4. theorem OAI.Problem367.mem_rootComplementFinset line 26
  5. theorem OAI.Problem367.ConnectedFinset.prefix_mem_of_root_mem line 32
  6. theorem OAI.Problem367.ConnectedFinset.filter_prefix_connected line 38
  7. theorem OAI.Problem367.ConnectedFinset.filter_not_prefix_connected line 78
  8. theorem OAI.Problem367.rootComponentFinset_connected line 107
  9. theorem OAI.Problem367.rootComplementFinset_connected line 113
  10. theorem OAI.Problem367.rootComponentFinset_union_complement line 118
  11. theorem OAI.Problem367.rootComponentFinset_disjoint_complement line 125
  12. theorem OAI.Problem367.root_component_crossing_edge line 132
  13. theorem OAI.Problem367.rootComponentFinset_mono line 151
  14. theorem OAI.Problem367.rootComplementFinset_mono line 157
  15. theorem OAI.Problem367.rootComponentFinset_exhausts line 163
  16. theorem OAI.Problem367.singleton_prefix_iff_cons line 169
  17. theorem OAI.Problem367.rootComponentFinset_eq_filter line 177
  18. theorem OAI.Problem367.rootComplementFinset_eq_sdiff line 185
  19. theorem OAI.Problem367.rootComponentFinset_root_mem line 192
  20. theorem OAI.Problem367.rootComplementFinset_root_mem line 197
  21. theorem OAI.Problem367.mem_inducedEdges_cut line 207
  22. theorem OAI.Problem367.inducedEdges_rootComponent_split line 213
  23. theorem OAI.Problem367.inducedEdges_rootComponent_disjoint line 256
  24. theorem OAI.Problem367.root_bridge_not_mem_inducedEdges_cut line 265