OAI/Probability/LatticeSurface/Convexity/RetainedShell.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RetainedShell.base line 287
  2. def OAI.RetainedShell.bulk line 289
  3. def OAI.RetainedShell.retained line 292
  4. def OAI.RetainedShell.retainedHeight line 294
  5. def OAI.RetainedShell.patch line 297
  6. def OAI.RetainedShell.assembled line 300
  7. def OAI.RetainedShell.shellData line 304
  8. def OAI.RetainedShell.remaining line 307
  9. def OAI.RetainedShell.fiber line 311
  10. def OAI.RetainedShell.shellDensity line 314
  11. lemma OAI.RetainedShell.mem_bulk line 324
  12. lemma OAI.RetainedShell.grid_coordinate_unique line 333
  13. lemma OAI.RetainedShell.block_unique line 342
  14. lemma OAI.RetainedShell.block_shell_not_bulk line 348
  15. lemma OAI.RetainedShell.adj_translate line 356
  16. lemma OAI.RetainedShell.interior_neighbor line 362
  17. lemma OAI.RetainedShell.bulk_subset line 368
  18. lemma OAI.RetainedShell.patch_zero line 375
  19. lemma OAI.RetainedShell.assembled_remaining line 378
  20. lemma OAI.RetainedShell.assembled_interior line 385
  21. lemma OAI.RetainedShell.assembled_on_block line 401
  22. lemma OAI.RetainedShell.assembled_zero_exterior line 410
  23. lemma OAI.RetainedShell.fiber_iff line 418
  24. theorem OAI.RetainedShell.density_product line 455