OAI/Geometry/IsometricImmersion/Estimates/LargestBlockLinearization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.HighEquation.fullBlockPartition line 13
2. theorem OAI.SmoothLocal.HighEquation.ordered_full_size_length_one line 25
3. theorem OAI.SmoothLocal.HighEquation.ordered_length_one_eq_full line 41
4. theorem OAI.SmoothLocal.HighEquation.ordered_nonfull_partSize_le line 61
5. def OAI.SmoothLocal.HighEquation.darbouxFaaTerm line 70
6. def OAI.SmoothLocal.HighEquation.directLinearization line 75
7. theorem OAI.SmoothLocal.HighEquation.fullBlockPartition_term line 81
8. theorem OAI.SmoothLocal.HighEquation.fullBlockPartition_actual_linearization line 89
9. theorem OAI.SmoothLocal.HighEquation.actualDarboux_extract_fullBlock line 101