OAI/Geometry/Immersion/ClosedSurface/AtlasDecomposition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.atlas_pair_margins_actual line 20
2. def OAI.ClosedSurfaceR4.selectedAmplitude line 63
3. def OAI.ClosedSurfaceR4.AtlasMetricDecomposition line 71
4. lemma OAI.ClosedSurfaceR4.assemble_selected_metric line 84
5. theorem OAI.ClosedSurfaceR4.fixed_atlas_polynomial_metric_decomposition_with_catalog line 121
6. theorem OAI.ClosedSurfaceR4.fixed_atlas_polynomial_metric_decomposition line 187