OAI/Geometry/CAT0Fillings/Reconstruction/ScalarCharts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.reindexFactor line 14
2. lemma OAI.CAT0Fillings.IntegerChart.jacobian_reindex line 20
3. lemma OAI.CAT0Fillings.IntegerChart.action_reindex line 32
4. lemma OAI.CAT0Fillings.Foundations.IntegerRectifiable.apply_reindex line 46
5. lemma OAI.CAT0Fillings.Slicing.NormalApprox.apply_reindex line 59
6. lemma OAI.CAT0Fillings.BorelCoefficients.borelAction_reindex line 81
7. lemma OAI.CAT0Fillings.BorelRestriction.restrictCurrent_reindex line 107
8. def OAI.CAT0Fillings.SliceReconstruction.scalarEquiv line 132
9. lemma OAI.CAT0Fillings.SliceReconstruction.scalarEquiv_apply line 134
10. lemma OAI.CAT0Fillings.SliceReconstruction.scalarEquiv_volume line 136
11. def OAI.CAT0Fillings.SliceReconstruction.scalarGraphChart line 141
12. lemma OAI.CAT0Fillings.SliceReconstruction.scalarGraphChart_image line 174
13. lemma OAI.CAT0Fillings.SliceReconstruction.scalarGraphChart_base_jacobian line 186
14. def OAI.CAT0Fillings.SliceReconstruction.scalarGraphFunction line 203
15. lemma OAI.CAT0Fillings.SliceReconstruction.scalarGraphChart_base_action line 206