OAI/Geometry/IsometricImmersion/Assembly/AssemblyProfiles.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SmoothLocal.Geometry.PatchAddress line 14
  2. instance OAI.SmoothLocal.Geometry.(instance at line 17) line 17
  3. abbrev OAI.SmoothLocal.Geometry.AssemblyProfileIndex line 24
  4. instance OAI.SmoothLocal.Geometry.assemblyProfileEncodable line 26
  5. def OAI.SmoothLocal.Geometry.patchAddressCarrier line 29
  6. def OAI.SmoothLocal.Geometry.patchAddressProfile line 32
  7. theorem OAI.SmoothLocal.Geometry.patchAddressCarriers_pairwise_disjoint line 35
  8. def OAI.SmoothLocal.Geometry.assemblyCarrier line 58
  9. def OAI.SmoothLocal.Geometry.assemblyProfile line 62
  10. theorem OAI.SmoothLocal.Geometry.assemblyProfile_contDiff line 66
  11. theorem OAI.SmoothLocal.Geometry.assemblyProfile_hasCompactSupport line 71
  12. theorem OAI.SmoothLocal.Geometry.assemblyProfile_tsupport_subset line 77
  13. theorem OAI.SmoothLocal.Geometry.assemblyCarriers_pairwise_disjoint line 83
  14. theorem OAI.SmoothLocal.Geometry.zero_not_mem_assemblyCarrier line 97
  15. def OAI.SmoothLocal.Geometry.enumeratedAssemblyProfile line 106
  16. theorem OAI.SmoothLocal.Geometry.enumeratedAssemblyProfile_encode line 111
  17. theorem OAI.SmoothLocal.Geometry.enumeratedAssemblyProfile_contDiff line 115
  18. theorem OAI.SmoothLocal.Geometry.enumeratedAssemblyProfile_hasCompactSupport line 124
  19. theorem OAI.SmoothLocal.Geometry.zero_not_mem_enumeratedAssemblyProfile_tsupport line 131
  20. theorem OAI.SmoothLocal.Geometry.enumeratedAssemblyProfile_zero_other line 139