OAI/Geometry/CAT0Fillings/Slices/FullSlices.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Slicing.NormalApprox.eq_zero_of_cost_zero line 18
2. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_zero line 25
3. lemma OAI.CAT0Fillings.Slicing.normalSlice_zero line 38
4. lemma OAI.CAT0Fillings.Slicing.normalSlice_eq_zero_outside line 47
5. lemma OAI.CAT0Fillings.Slicing.NormalApprox.cost_congr line 57
6. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_total_coarea_bound line 63
7. lemma OAI.CAT0Fillings.Slicing.normalSlice_cost_upper line 87
8. lemma OAI.CAT0Fillings.Slicing.measurable_normalSlice_cost line 126
9. theorem OAI.CAT0Fillings.Slicing.normalSlice_cost_integrable line 137
10. def OAI.CAT0Fillings.Slicing.fullSlice line 204
11. lemma OAI.CAT0Fillings.Slicing.fullSlice_approx line 210
12. lemma OAI.CAT0Fillings.Slicing.fullSlice_integral line 217
13. lemma OAI.CAT0Fillings.Slicing.measurable_fullSlice_family line 221
14. lemma OAI.CAT0Fillings.Slicing.measurable_fullSlice line 242
15. lemma OAI.CAT0Fillings.Slicing.measurable_fullSlice_cost line 251
16. theorem OAI.CAT0Fillings.Slicing.fullSlice_cost_integrable line 256
17. lemma OAI.CAT0Fillings.Slicing.fullSlice_eval_integrable line 311
18. lemma OAI.CAT0Fillings.Slicing.normalSlice_integral line 337
19. theorem OAI.CAT0Fillings.Slicing.fullSlice_action_integral line 353