OAI/Geometry/TamingCompatibility/Hodge/HodgeSmoothInverse.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothShift_cube_bijective line 23
2. def OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothInverse line 35
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothInverse_left line 40
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothInverse_right line 43
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeSmoothInverse_spec line 47
6. def OAI.TamingCompatibility.GeometricHilbert.hodgeDistributionInverse line 70
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeDistributionInverse_bound line 76
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeDistributionInverse_represents line 86
9. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCubeRepresents_unique line 104
10. lemma OAI.TamingCompatibility.unitMeasureCurrent_finite_bound line 131
11. def OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionSource line 146
12. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionSource_anti line 152
13. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionSource_closed line 167
14. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeCorrectionSource_bound line 195