OAI/Analysis/StrictMeans/QuadraticHomotopy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.Grid.fderiv_apply_of_line line 14
  2. lemma OAI.StrictInverseFirstPower.Grid.derivative_homotopy_regular line 22
  3. def OAI.StrictInverseFirstPower.Grid.quadratic line 48
  4. def OAI.StrictInverseFirstPower.Grid.quadraticFamily line 51
  5. lemma OAI.StrictInverseFirstPower.Grid.quadraticFamily_contDiff line 54
  6. lemma OAI.StrictInverseFirstPower.Grid.quadraticFamily_dx line 65
  7. lemma OAI.StrictInverseFirstPower.Grid.quadraticFamily_dy line 81
  8. lemma OAI.StrictInverseFirstPower.Grid.quadraticFamily_regular line 97