OAI/Analysis/StrictMeans/GridComplex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.Grid.chainSpace_mono line 10
  2. lemma OAI.StrictInverseFirstPower.Grid.chainSpace_shift_x line 15
  3. lemma OAI.StrictInverseFirstPower.Grid.chainSpace_shift_y line 25
  4. lemma OAI.StrictInverseFirstPower.Grid.chainSpace_shift_xy line 35
  5. lemma OAI.StrictInverseFirstPower.Grid.boundary₁_mem line 43
  6. lemma OAI.StrictInverseFirstPower.Grid.faceH_mem line 56
  7. lemma OAI.StrictInverseFirstPower.Grid.faceV_mem line 60
  8. lemma OAI.StrictInverseFirstPower.Grid.faceD_mem line 64
  9. def OAI.StrictInverseFirstPower.Grid.edgeBoundary line 69
  10. def OAI.StrictInverseFirstPower.Grid.faceBoundary line 78
  11. lemma OAI.StrictInverseFirstPower.Grid.faceBoundary_injective line 89
  12. lemma OAI.StrictInverseFirstPower.Grid.boundary_exact line 97