OAI/Probability/CriticalPercolation/Criticality/CutInside.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.Sharpness.cutInside line 18
  2. def OAI.CriticalPercolation.Sharpness.cutOutside line 21
  3. def OAI.CriticalPercolation.Sharpness.IsCut line 24
  4. lemma OAI.CriticalPercolation.Sharpness.cut_ends line 26
  5. lemma OAI.CriticalPercolation.Sharpness.cut_orientation line 33
  6. lemma OAI.CriticalPercolation.Sharpness.boundaryReach_iff_cut line 45
  7. def OAI.CriticalPercolation.Sharpness.internalIncident line 56
  8. def OAI.CriticalPercolation.Sharpness.internalCluster line 59
  9. lemma OAI.CriticalPercolation.Sharpness.internalCluster_self line 62
  10. lemma OAI.CriticalPercolation.Sharpness.internalCluster_subset line 65
  11. lemma OAI.CriticalPercolation.Sharpness.internal_adj_eq line 71
  12. lemma OAI.CriticalPercolation.Sharpness.internalCluster_eq_of_incident line 86
  13. lemma OAI.CriticalPercolation.Sharpness.dependsOn_internalCluster line 96
  14. lemma OAI.CriticalPercolation.Sharpness.last_exit line 103
  15. lemma OAI.CriticalPercolation.Sharpness.internalCluster_exit line 121
  16. lemma OAI.CriticalPercolation.Sharpness.cut_not_internalIncident line 136
  17. lemma OAI.CriticalPercolation.Sharpness.delete_update_incident line 144