OAI/Geometry/CAT0Fillings/Reconstruction/Slices.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.SliceReconstruction.centeredSlopeSet line 13
2. lemma OAI.CAT0Fillings.SliceReconstruction.isClosed_centeredSlopeSet line 17
3. abbrev OAI.CAT0Fillings.SliceReconstruction.PieceIndex line 43
4. def OAI.CAT0Fillings.SliceReconstruction.slopePiece line 45
5. lemma OAI.CAT0Fillings.SliceReconstruction.isCompact_slopePiece line 49
6. lemma OAI.CAT0Fillings.SliceReconstruction.lipschitzOnWith_slopePiece line 55
7. lemma OAI.CAT0Fillings.SliceReconstruction.mem_iUnion_slopePiece_of_differentiableAt line 67
8. lemma OAI.CAT0Fillings.SliceReconstruction.ae_mem_iUnion_slopePiece line 89
9. lemma OAI.CAT0Fillings.Slicing.restrictCurrent_sub_of_subset line 105
10. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_increment line 123
11. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_increment_bound line 142
12. def OAI.CAT0Fillings.Slicing.sliceController line 177
13. lemma OAI.CAT0Fillings.Slicing.monotone_sliceController line 183
14. lemma OAI.CAT0Fillings.Slicing.sliceController_sub line 190
15. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_controller_bound line 207
16. theorem OAI.CAT0Fillings.Slicing.exists_compact_slice_lipschitz_pieces line 235