OAI/Geometry/CAT0Fillings/Isoperimetry/SmallCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.exists_smallCell_cut line 17
2. lemma OAI.CAT0Fillings.restrictCurrent_add_compl line 63
3. lemma OAI.CAT0Fillings.mass_restriction_add_compl line 71
4. lemma OAI.CAT0Fillings.integral_dist_restriction_ball_le line 79
5. lemma OAI.CAT0Fillings.integral_dist_le_diam line 102
6. theorem OAI.CAT0Fillings.finite_cell_filling line 130