OAI/Probability/UnimodularPercolation/Encounter/Surgery.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exterior branches and finite encounter surgery.

  1. theorem OAI.Percolation.infinite_cluster_sdiff_contains line 20
  2. theorem OAI.Percolation.conn_eq_of_no_incident line 27
  3. theorem OAI.Percolation.cluster_singleton_of_no_incident line 35
  4. theorem OAI.Percolation.deleted_cluster_singleton line 42
  5. theorem OAI.Percolation.conn_exterior_attachment line 49
  6. theorem OAI.Percolation.infinite_exterior_attachment line 76
  7. theorem OAI.Percolation.exists_finite_connected_envelope line 89
  8. theorem OAI.Percolation.deleted_envelope_separated line 107
  9. theorem OAI.Percolation.encounter_surgery_of_attachments line 126
  10. theorem OAI.Percolation.encounter_surgery_of_three line 189
  11. theorem OAI.Percolation.three_of_infinite_count line 214