OAI/Probability/FreeIsing/Trees/ConnectedPercolation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ConnectedPercolation.deepestVertexOr line 9
  2. lemma OAI.Problem367.ConnectedPercolation.deepestVertexOr_mem line 14
  3. lemma OAI.Problem367.ConnectedPercolation.le_deepestVertexOr_length line 19
  4. def OAI.Problem367.ConnectedPercolation.prefixCandidates line 25
  5. lemma OAI.Problem367.ConnectedPercolation.mem_prefixCandidates line 30
  6. def OAI.Problem367.ConnectedPercolation.gate line 35
  7. lemma OAI.Problem367.ConnectedPercolation.gate_of_mem line 38
  8. lemma OAI.Problem367.ConnectedPercolation.gate_of_no_prefix line 48
  9. lemma OAI.Problem367.ConnectedPercolation.prefixCandidates_append_of_not_mem line 57
  10. lemma OAI.Problem367.ConnectedPercolation.gate_append_cases line 82
  11. lemma OAI.Problem367.ConnectedPercolation.gate_adj_cases line 109
  12. theorem OAI.Problem367.ConnectedFinset.reflTransGen_restrict_iff line 124
  13. theorem OAI.Problem367.ConnectedFinset.cluster_inter_eq line 155