OAI/Geometry/IsometricImmersion/Assembly/EnumeratedPatchTensors.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.patchAddressCenter line 14
  2. def OAI.SmoothLocal.Geometry.patchAddressMatrix line 16
  3. theorem OAI.SmoothLocal.Geometry.patchAddressMatrix_isUnit line 19
  4. def OAI.SmoothLocal.Geometry.patchTensorIndex line 22
  5. theorem OAI.SmoothLocal.Geometry.patchTensorIndex_injective line 25
  6. def OAI.SmoothLocal.Geometry.patchTensorAddress line 29
  7. theorem OAI.SmoothLocal.Geometry.patchTensorAddress_index line 34
  8. theorem OAI.SmoothLocal.Geometry.patchTensorAddress_eq_some_iff line 38
  9. def OAI.SmoothLocal.Geometry.patchAddressTensor line 55
  10. theorem OAI.SmoothLocal.Geometry.patchAddressTensor_contDiff line 58
  11. theorem OAI.SmoothLocal.Geometry.patchAddressTensor_tsupport_subset line 64
  12. theorem OAI.SmoothLocal.Geometry.patchAddressCarrier_isCompact line 75
  13. theorem OAI.SmoothLocal.Geometry.patchAddressTensor_hasCompactSupport line 78
  14. def OAI.SmoothLocal.Geometry.enumeratedPatchTensor line 83
  15. def OAI.SmoothLocal.Geometry.enumeratedPatchCarrier line 88
  16. theorem OAI.SmoothLocal.Geometry.enumeratedPatchTensor_index line 93
  17. theorem OAI.SmoothLocal.Geometry.enumeratedPatchCarrier_index line 97
  18. theorem OAI.SmoothLocal.Geometry.enumeratedPatchTensor_contDiff line 101
  19. theorem OAI.SmoothLocal.Geometry.enumeratedPatchCarrier_isCompact line 110
  20. theorem OAI.SmoothLocal.Geometry.enumeratedPatchTensor_tsupport_subset line 115
  21. theorem OAI.SmoothLocal.Geometry.enumeratedPatchTensor_hasCompactSupport line 122
  22. theorem OAI.SmoothLocal.Geometry.enumeratedPatchCarriers_pairwise_disjoint line 127
  23. theorem OAI.SmoothLocal.Geometry.zero_not_mem_enumeratedPatchCarrier line 143
  24. theorem OAI.SmoothLocal.Geometry.enumeratedPatchCarrier_disjoint_disk line 151
  25. def OAI.SmoothLocal.Geometry.patchTensorBudgetNeighborhood line 159
  26. theorem OAI.SmoothLocal.Geometry.patchTensorBudgetNeighborhood_isOpen line 163
  27. theorem OAI.SmoothLocal.Geometry.zero_mem_patchTensorBudgetNeighborhood line 167
  28. theorem OAI.SmoothLocal.Geometry.enumeratedPatchTensor_diagonal_bound line 171