OAI/Geometry/CAT0Fillings/Slices/Limits.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.Slicing.restrictCurrent_mass_le line 18
2. lemma OAI.CAT0Fillings.Slicing.restrictCurrent_empty line 24
3. lemma OAI.CAT0Fillings.Slicing.restrictCurrent_univ line 30
4. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_eq_zero_outside line 38
5. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_bound_uniform line 58
6. lemma OAI.CAT0Fillings.Slicing.superlevelSlice_integral line 83
7. theorem OAI.CAT0Fillings.Slicing.superlevelSlice_integral_of_bounded_weak_limit line 97
8. lemma OAI.CAT0Fillings.Slicing.mass_le_liminf_upper line 166
9. lemma OAI.CAT0Fillings.Slicing.exists_integrable_mass_upper_of_ae_weak_limit line 186
10. theorem OAI.CAT0Fillings.Slicing.superlevelSlice_mass_bound_of_bounded_weak_limit line 222