OAI/Analysis/StrictMeans/SmoothMorseIndex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StrictInverseFirstPower.Grid.second line 11
2. def OAI.StrictInverseFirstPower.Grid.hessianDet line 13
3. def OAI.StrictInverseFirstPower.Grid.morseSign line 15
4. lemma OAI.StrictInverseFirstPower.Grid.smooth_morse_local_index line 17