OAI/Geometry/TamingCompatibility/DifferentialForms/Space.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.SmoothAlmostComplex.Space line 16
2. abbrev OAI.TamingCompatibility.SmoothAlmostComplex.Model line 17
3. structure OAI.TamingCompatibility.SmoothAlmostComplex.AlmostComplexStructure line 22
4. lemma OAI.TamingCompatibility.SmoothAlmostComplex.contMDiffAt_localConstant line 30
5. lemma OAI.TamingCompatibility.SmoothAlmostComplex.contMDiffOn_coord_apply line 41
6. def OAI.TamingCompatibility.SmoothAlmostComplex.coord line 54
7. lemma OAI.TamingCompatibility.SmoothAlmostComplex.contDiffOn_coord_chart line 60
8. def OAI.TamingCompatibility.ManifoldForms.jAction line 87
9. lemma OAI.TamingCompatibility.ManifoldForms.pullback_jAction_chart line 90
10. theorem OAI.TamingCompatibility.ManifoldForms.Smooth.jAction line 121
11. lemma OAI.TamingCompatibility.IsSmooth.jAction line 136
12. lemma OAI.TamingCompatibility.IsSmooth.invariantPart line 141
13. lemma OAI.TamingCompatibility.IsSmooth.antiInvariantPart line 145