OAI/Geometry/CAT0Fillings/Currents/AffineCalculus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.boundedLipSubmodule line 34
2. lemma OAI.CAT0Fillings.bl_coe_update line 43
3. lemma OAI.CAT0Fillings.bl_update_tail_zero line 50
4. lemma OAI.CAT0Fillings.bl_update_tail_succ line 57
5. def OAI.CAT0Fillings.IsMetricCurrent.fullMultilinear line 63
6. def OAI.CAT0Fillings.pairLinearCombination line 98
7. def OAI.CAT0Fillings.IsMetricCurrent.affineCoefficients line 104
8. lemma OAI.CAT0Fillings.pairMultilinear_hasDeriv line 119
9. lemma OAI.CAT0Fillings.IsMetricCurrent.affineCoefficients_apply line 128
10. lemma OAI.CAT0Fillings.IsMetricCurrent.hasDeriv_fullAffine line 135