OAI/Probability/LatticeSurface/Coercivity/FilledHull.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SparseHoles.box line 14
  2. def OAI.SparseHoles.anchor line 17
  3. def OAI.SparseHoles.safeReach line 19
  4. def OAI.SparseHoles.exterior line 22
  5. def OAI.SparseHoles.filled line 25
  6. lemma OAI.SparseHoles.safe_refl line 29
  7. lemma OAI.SparseHoles.safe_symm line 32
  8. lemma OAI.SparseHoles.safe_trans line 36
  9. lemma OAI.SparseHoles.safe_adj line 47
  10. lemma OAI.SparseHoles.safe_start line 51
  11. lemma OAI.SparseHoles.safe_end line 55
  12. lemma OAI.SparseHoles.safe_int_line line 58
  13. lemma OAI.SparseHoles.safe_row line 74
  14. lemma OAI.SparseHoles.safe_col line 77
  15. lemma OAI.SparseHoles.mem_box line 80
  16. lemma OAI.SparseHoles.anchor_not_mem line 85
  17. lemma OAI.SparseHoles.outside_box_exterior line 91
  18. lemma OAI.SparseHoles.mem_filled line 118
  19. lemma OAI.SparseHoles.subset_filled line 124
  20. lemma OAI.SparseHoles.filled_subset_box line 131
  21. lemma OAI.SparseHoles.exterior_adj line 135
  22. lemma OAI.SparseHoles.lift_walk line 139
  23. lemma OAI.SparseHoles.exterior_connected line 149
  24. lemma OAI.SparseHoles.filled_complement_connected line 163
  25. lemma OAI.SparseHoles.grid_connected line 171
  26. lemma OAI.SparseHoles.reach_cluster_walk line 178
  27. lemma OAI.SparseHoles.reach_cluster line 195
  28. lemma OAI.SparseHoles.filled_star_connected line 203
  29. theorem OAI.SparseHoles.filled_rim_paths line 220