OAI/Analysis/StrictMeans/LatticeGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.latticeCoord line 11
  2. lemma OAI.StrictInverseFirstPower.Grid.latticeCoord_ex line 16
  3. lemma OAI.StrictInverseFirstPower.Grid.latticeCoord_ey line 17
  4. lemma OAI.StrictInverseFirstPower.Grid.latticeCoord_re line 18
  5. lemma OAI.StrictInverseFirstPower.Grid.latticeCoord_im line 19
  6. def OAI.StrictInverseFirstPower.Grid.meshPoint line 21
  7. lemma OAI.StrictInverseFirstPower.Grid.meshPoint_add line 23
  8. lemma OAI.StrictInverseFirstPower.Grid.meshPoint_sub line 26
  9. lemma OAI.StrictInverseFirstPower.Grid.StarCertificate.toRegularStar line 30
  10. lemma OAI.StrictInverseFirstPower.Grid.latticeCoord_injective line 36
  11. lemma OAI.StrictInverseFirstPower.Grid.meshPoint_injective line 43
  12. lemma OAI.StrictInverseFirstPower.Grid.meshPoint_bounded_preimage line 47
  13. lemma OAI.StrictInverseFirstPower.Grid.norm_latticeCoord_star line 70
  14. lemma OAI.StrictInverseFirstPower.Grid.meshPoint_star_dist line 86
  15. lemma OAI.StrictInverseFirstPower.Grid.meshBoundary_annulus line 94