OAI/Geometry/TamingCompatibility/DifferentialForms/ContDiffLinearEmbedding.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TamingCompatibility.FormSmoothness.contDiffOn_of_linear_embedding line 37
  2. lemma OAI.TamingCompatibility.FormSmoothness.ContDiffOn.compAlternating line 47
  3. lemma OAI.TamingCompatibility.FormSmoothness.contDiff_compAlternating line 73
  4. lemma OAI.TamingCompatibility.FormSmoothness.ContDiffAt.compAlternating line 80
  5. abbrev OAI.TamingCompatibility.ManifoldForms.Space line 92
  6. abbrev OAI.TamingCompatibility.ManifoldForms.Model line 93
  7. abbrev OAI.TamingCompatibility.ManifoldForms.Form line 95
  8. def OAI.TamingCompatibility.ManifoldForms.pullback line 101
  9. def OAI.TamingCompatibility.ManifoldForms.Smooth line 104
  10. def OAI.TamingCompatibility.ManifoldForms.Closed line 108
  11. def OAI.TamingCompatibility.ManifoldForms.exteriorDerivative line 113
  12. lemma OAI.TamingCompatibility.ManifoldForms.extDerivWithin_eq_of_mem line 116
  13. lemma OAI.TamingCompatibility.ManifoldForms.pullback_comp line 123
  14. lemma OAI.TamingCompatibility.ManifoldForms.pullback_congr_eventually line 133
  15. lemma OAI.TamingCompatibility.ManifoldForms.smooth_chart line 142
  16. theorem OAI.TamingCompatibility.ManifoldForms.smooth_of_charts line 146
  17. theorem OAI.TamingCompatibility.ManifoldForms.pullback_exteriorDerivative line 183
  18. theorem OAI.TamingCompatibility.ManifoldForms.Smooth.exteriorDerivative line 233
  19. theorem OAI.TamingCompatibility.ManifoldForms.closed_iff_exteriorDerivative_eq_zero line 243
  20. theorem OAI.TamingCompatibility.ManifoldForms.exteriorDerivative_square line 258
  21. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.closed_exteriorDerivative line 277
  22. lemma OAI.TamingCompatibility.ManifoldForms.pullback_add line 282
  23. lemma OAI.TamingCompatibility.ManifoldForms.pullback_smul line 286
  24. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.zero line 290
  25. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.add line 296
  26. lemma OAI.TamingCompatibility.ManifoldForms.Smooth.smul line 303
  27. lemma OAI.TamingCompatibility.ManifoldForms.exteriorDerivative_add line 308
  28. lemma OAI.TamingCompatibility.ManifoldForms.exteriorDerivative_smul line 322
  29. def OAI.TamingCompatibility.ManifoldForms.smoothForms line 329
  30. def OAI.TamingCompatibility.ManifoldForms.d line 336
  31. lemma OAI.TamingCompatibility.ManifoldForms.d_square line 341
  32. def OAI.TamingCompatibility.ManifoldForms.closedForms line 344
  33. lemma OAI.TamingCompatibility.ManifoldForms.mem_closedForms_iff line 348
  34. lemma OAI.TamingCompatibility.ManifoldForms.d_mem_closedForms line 353