OAI/Probability/FreeIsing/Estimates/LeafDeletion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.reflTransGen_erase_of_unique_neighbor line 9
  2. theorem OAI.Problem367.reflTransGen_connected_erase_of_leaf line 46
  3. theorem OAI.Problem367.connectedFinset_erase_of_leaf line 69
  4. theorem OAI.Problem367.treeAdj_unique_neighbor_of_max_length line 81
  5. theorem OAI.Problem367.connectedFinset_erase_of_max_length line 100
  6. theorem OAI.Problem367.inducedEdges_eq_insert_erase_of_max_length line 107
  7. theorem OAI.Problem367.inducedEdges_eq_insert_erase_of_unique_lower_neighbor line 136