OAI/Geometry/CAT0Fillings/Currents/CanonicalMass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.MassMeasure.weighted line 33
2. lemma OAI.CAT0Fillings.MassMeasure.weighted_finite line 36
3. lemma OAI.CAT0Fillings.MassMeasure.integral_weighted line 42
4. lemma OAI.CAT0Fillings.MassMeasure.weighted_total line 50
5. lemma OAI.CAT0Fillings.MassMeasure.controls_splice line 57
6. lemma OAI.CAT0Fillings.MassMeasure.integral_cutoff_le line 94
7. lemma OAI.CAT0Fillings.MassMeasure.measure_closed_le line 117
8. lemma OAI.CAT0Fillings.MassMeasure.measure_le line 143
9. lemma OAI.CAT0Fillings.MassMeasure.measure_unique line 152
10. def OAI.CAT0Fillings.MassMeasure.currentMassMeasure line 157
11. instance OAI.CAT0Fillings.MassMeasure.currentMassMeasure_finite line 160
12. lemma OAI.CAT0Fillings.MassMeasure.currentMassMeasure_controls line 164
13. lemma OAI.CAT0Fillings.MassMeasure.currentMassMeasure_total line 168
14. lemma OAI.CAT0Fillings.MassMeasure.currentMassMeasure_le line 172