OAI/Probability/LatticeSurface/Convexity/RetainedCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RetainedShell.Indices line 319
2. def OAI.RetainedShell.indexMap line 321
3. lemma OAI.RetainedShell.indexMap_bijective line 326
4. def OAI.RetainedShell.indexEquiv line 362
5. def OAI.RetainedShell.split line 366
6. lemma OAI.RetainedShell.preserving_split line 373
7. lemma OAI.RetainedShell.split_fst line 379
8. lemma OAI.RetainedShell.split_snd line 385
9. lemma OAI.RetainedShell.continuous_split line 392
10. lemma OAI.RetainedShell.split_assembled line 406
11. lemma OAI.RetainedShell.inverse_height line 418
12. lemma OAI.RetainedShell.body_fiber line 431