OAI/Probability/LatticeSurface/Convexity/BoundedBase.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExtremalEdges.Free line 15
2. instance OAI.ExtremalEdges.(instance at line 17) line 17
3. def OAI.ExtremalEdges.restore line 20
4. def OAI.ExtremalEdges.conditionalBody line 23
5. lemma OAI.ExtremalEdges.continuous_restore line 27
6. lemma OAI.ExtremalEdges.closed_conditionalBody line 34
7. lemma OAI.ExtremalEdges.preserving_piOptionReal line 41
8. def OAI.ExtremalEdges.coordinateIndex line 48
9. def OAI.ExtremalEdges.splitCoordinate line 68
10. lemma OAI.ExtremalEdges.preserving_splitCoordinate line 73
11. lemma OAI.ExtremalEdges.coordinate_restore line 77
12. lemma OAI.ExtremalEdges.bound_along_walk line 94
13. lemma OAI.ExtremalEdges.volume_zeroBody_pos line 106