OAI/Geometry/CAT0Fillings/Radial/ChartMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.IntegerChart.radialJacobian line 31
2. theorem OAI.CAT0Fillings.IntegerChart.ae_radial_jacobian_bound line 39
3. theorem OAI.CAT0Fillings.IntegerChart.radial_push_mass_le line 97