OAI/Probability/CriticalPercolation/GraphGeometry/MarkConnectivity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CriticalPercolation.infinite_cluster_of_reached_marks line 15
  2. lemma OAI.CriticalPercolation.BondGraph.percolation_of_infinite_marks line 41
  3. theorem OAI.CriticalPercolation.BondGraph.no_subcritical_good_exploration line 55