OAI/Geometry/CylinderCovering/Barycentric/LocalDictionary.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RadialCoordinates.Hpos line 12
  2. lemma OAI.RadialCoordinates.Hne line 13
  3. lemma OAI.RadialCoordinates.Hsq line 14
  4. theorem OAI.RadialCoordinates.canonicalEmbedding_norm line 16
  5. def OAI.RadialCoordinates.canonicalEmbeddingIsometry line 25
  6. theorem OAI.RadialCoordinates.canonicalScale_pos line 28
  7. theorem OAI.RadialCoordinates.canonicalToBary_eq line 32
  8. theorem OAI.RadialCoordinates.angular_point line 39
  9. theorem OAI.RadialCoordinates.angular_mem_cell_iff line 44
  10. theorem OAI.RadialCoordinates.angular_tags line 51
  11. theorem OAI.RadialCoordinates.angular_inverse line 56
  12. theorem OAI.RadialCoordinates.inverse_angular line 58
  13. theorem OAI.RadialCoordinates.lowerPoint_toBary line 60
  14. theorem OAI.RadialCoordinates.upperPoint_toBary line 69
  15. theorem OAI.RadialCoordinates.lowerLocalSweep_image line 78
  16. theorem OAI.RadialCoordinates.upperLocalSweep_image line 107
  17. theorem OAI.RadialCoordinates.canonicalEmbedding_lower_raw line 136
  18. theorem OAI.RadialCoordinates.canonicalEmbedding_upper_raw line 144
  19. theorem OAI.RadialCoordinates.normalized_positive_smul line 153
  20. theorem OAI.RadialCoordinates.canonicalEmbedding_lowerAxis line 161
  21. theorem OAI.RadialCoordinates.canonicalEmbedding_upperAxis line 169
  22. theorem OAI.RadialCoordinates.canonicalScale_sq line 177
  23. theorem OAI.RadialCoordinates.canonicalCap_continuous line 182
  24. theorem OAI.RadialCoordinates.canonicalCap_nonneg line 186
  25. theorem OAI.RadialCoordinates.barycentric_midpoint_tagged line 190
  26. theorem OAI.RadialCoordinates.canonical_midpoint_tagged line 199
  27. theorem OAI.RadialCoordinates.canonicalCap_eq line 203
  28. theorem OAI.RadialCoordinates.canonical_physicalCost line 208