OAI/Probability/LatticeSurface/Geometry/BlockGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RetainedShell.ordinary line 352
2. lemma OAI.TriangularLipschitz.global_lipschitz line 359
3. lemma OAI.TriangularLipschitz.latticeDist_add_left line 382
4. lemma OAI.RetainedShell.base_enlarged line 394
5. lemma OAI.RetainedShell.mem_ordinary line 399
6. lemma OAI.RetainedShell.block_enlarged line 410
7. lemma OAI.RetainedShell.block_translate line 417
8. lemma OAI.RetainedShell.ordinary_free line 423
9. lemma OAI.RetainedShell.face_source line 428
10. lemma OAI.RetainedShell.neighbor_source line 432
11. lemma OAI.RetainedShell.face_in_box line 436
12. theorem OAI.RetainedShell.pin_block_faces line 446
13. theorem OAI.RetainedShell.ordinary_good line 477