OAI/Geometry/TamingCompatibility/Hodge/HodgeCutoffFamilies.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.principal line 18
2. def OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.first line 21
3. def OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.zero line 26
4. lemma OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.principal_smooth line 32
5. lemma OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.first_smooth line 41
6. lemma OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.zero_smooth line 53
7. lemma OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.principal_center line 68
8. lemma OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.principal_dpos_zero line 73
9. lemma OAI.TamingCompatibility.GeometricHilbert.CutoffFamilies.first_center line 92