OAI/Geometry/TamingCompatibility/Hodge/HodgeSmoothingCover.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingPatch line 23
  2. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingPatch.source line 31
  3. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingPatch.source_open line 34
  4. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingPatch.source_subset line 38
  5. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingPatch.source_image_subset line 40
  6. lemma OAI.TamingCompatibility.GeometricHilbert.exists_hodgeSmoothingPatch line 45
  7. structure OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover line 54
  8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothingCover_nonempty line 60
  9. def OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothingCover line 74
  10. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.coordinateSupport line 97
  11. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.coordinateSupport_compact line 100
  12. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.coordinateSupport_neighborhood line 104
  13. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.coordinateSupport_target line 109
  14. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.weightFunction line 114
  15. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.weightFunction_smooth_compact line 118
  16. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.weightFunction_support line 129
  17. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.weight line 139
  18. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.weight_support line 142
  19. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.weight_compact line 145
  20. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.weight_chart line 148
  21. def OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.basisForm line 157
  22. lemma OAI.TamingCompatibility.GeometricHilbert.HodgeSmoothingCover.basisForm_zero line 163