OAI/Geometry/CAT0Fillings/Slices/FullCarrier.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Slicing.boundedLip_sub_const line 19
2. lemma OAI.CAT0Fillings.Slicing.weightedCurrent_boundedLip_isMetricCurrent line 25
3. lemma OAI.CAT0Fillings.Slicing.weightedCurrent_boundedLip_apply line 34
4. lemma OAI.CAT0Fillings.Slicing.NormalApprox.metric line 41
5. lemma OAI.CAT0Fillings.Slicing.massMeasure_normalSlice_nonzero_zero line 46
6. lemma OAI.CAT0Fillings.Slicing.massMeasure_fullSlice_nonzero_zero line 65
7. lemma OAI.CAT0Fillings.Slicing.ae_superlevelSlice_weighted_integral line 76
8. lemma OAI.CAT0Fillings.Slicing.NormalApprox.ae_superlevelSlice_weighted line 88
9. lemma OAI.CAT0Fillings.Slicing.ae_normalSlice_mul_level line 110
10. theorem OAI.CAT0Fillings.Slicing.ae_normalSlice_mass_level line 127
11. lemma OAI.CAT0Fillings.Slicing.level_eval_of_carrier line 162
12. lemma OAI.CAT0Fillings.Slicing.ae_fullSlice_level_eval line 174
13. lemma OAI.CAT0Fillings.Slicing.ae_fullSlice_mass_level line 201
14. abbrev OAI.CAT0Fillings.Slicing.coordinateMap line 228
15. lemma OAI.CAT0Fillings.Slicing.ae_fullSlice_mass_fiber line 230
16. lemma OAI.CAT0Fillings.Slicing.ae_fullSlice_weighted line 242
17. lemma OAI.CAT0Fillings.Slicing.fullSlice_weighted_integral line 255