OAI/Analysis/StrictMeans/CanonicalIndex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.canonicalMin line 10
  2. def OAI.StrictInverseFirstPower.Grid.canonicalSaddle line 12
  3. def OAI.StrictInverseFirstPower.Grid.minVertex line 15
  4. def OAI.StrictInverseFirstPower.Grid.saddleVertex line 16
  5. lemma OAI.StrictInverseFirstPower.Grid.canonicalMin_index line 18
  6. lemma OAI.StrictInverseFirstPower.Grid.canonicalSaddle_index line 31
  7. lemma OAI.StrictInverseFirstPower.Grid.canonicalMin_sum line 44
  8. lemma OAI.StrictInverseFirstPower.Grid.canonicalSaddle_sum line 49