OAI/Geometry/CAT0Fillings/Currents/CycleDifference.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.mixedTuple line 34
2. lemma OAI.CAT0Fillings.MultilinearMap.sub_eq_sum_update line 37
3. lemma OAI.CAT0Fillings.IsMetricCurrent.cycle_difference line 53
4. lemma OAI.CAT0Fillings.IsMetricCurrent.cycle_difference_bound line 64
5. lemma OAI.CAT0Fillings.IsMetricCurrent.cycle_time_lipschitz line 98