OAI/Geometry/CAT0Fillings/Rearrangement/Inverse.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.fillingCoefficient_pos line 14
2. lemma OAI.CAT0Fillings.ball_filling_identity line 19
3. lemma OAI.CAT0Fillings.perimeter_of_small_isoperimetry line 36
4. def OAI.CAT0Fillings.Rearrangement.radialInverse line 70
5. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_bdd line 73
6. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_nonneg line 76
7. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_le line 79
8. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_antitone line 85
9. lemma OAI.CAT0Fillings.Rearrangement.mem_of_lt_radialInverse line 93
10. lemma OAI.CAT0Fillings.Rearrangement.radius_le_of_inverse_lt line 105
11. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_lipschitz line 112
12. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_superlevel line 168
13. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_zero_outside line 187
14. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_at_zero line 197
15. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_radius_identity line 207
16. lemma OAI.CAT0Fillings.Rearrangement.radialInverse_fiber line 229