OAI/Analysis/StrictMeans/GridLink.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.bit line 8
  2. def OAI.StrictInverseFirstPower.Grid.linkIndex line 10
  3. def OAI.StrictInverseFirstPower.Grid.signBound line 15
  4. lemma OAI.StrictInverseFirstPower.Grid.linkIndex_rotate line 17
  5. lemma OAI.StrictInverseFirstPower.Grid.regular_link_xpos line 21
  6. lemma OAI.StrictInverseFirstPower.Grid.regular_link_xneg line 33
  7. lemma OAI.StrictInverseFirstPower.Grid.linkIndex_reverse line 47
  8. lemma OAI.StrictInverseFirstPower.Grid.regular_link line 51