OAI/Probability/FreeIsing/Trees/ConnectedExhaustion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ConnectedHull.hull_mono line 12
  2. def OAI.Problem367.connectedExhaustion line 22
  3. theorem OAI.Problem367.connectedExhaustion_connected line 26
  4. theorem OAI.Problem367.mem_connectedExhaustion line 30
  5. theorem OAI.Problem367.connectedExhaustion_monotone line 35
  6. theorem OAI.Problem367.eventually_mem_connectedExhaustion line 42
  7. theorem OAI.Problem367.eventually_subset_connectedExhaustion line 49
  8. theorem OAI.Problem367.exists_connected_exhaustion line 59