OAI/Geometry/CAT0Fillings/Gradient/CyclePairing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.BoundedLip.memLp line 13
2. lemma OAI.CAT0Fillings.ChartGeometry.integerRectifiable line 27
3. lemma OAI.CAT0Fillings.ChartGeometry.abs_pairing_gradient_cycle_le line 30
4. lemma OAI.CAT0Fillings.ChartGeometry.pairing_eq_zero_of_gradient_limit line 57
5. lemma OAI.CAT0Fillings.ChartGeometry.testWeight_eq_zero_of_pairings line 76
6. lemma OAI.CAT0Fillings.vecCons_omitted_rows line 104
7. lemma OAI.CAT0Fillings.component_zero_of_omitted_det line 118