OAI/Geometry/TamingCompatibility/DifferentialForms/Linear.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.ExteriorForms.oneLinear line 14
  2. lemma OAI.TamingCompatibility.ExteriorForms.oneLinear_apply line 15
  3. def OAI.TamingCompatibility.ExteriorForms.wedgeTwo line 22
  4. lemma OAI.TamingCompatibility.ExteriorForms.volumeSquare_apply_vec line 25
  5. lemma OAI.TamingCompatibility.ExteriorForms.volumeSquare_comp line 32
  6. lemma OAI.TamingCompatibility.ExteriorForms.wedgeTwo_comp line 43
  7. lemma OAI.TamingCompatibility.ExteriorForms.wedgeTwo_apply line 54
  8. lemma OAI.TamingCompatibility.ExteriorForms.wedgeOne_apply_four line 61
  9. lemma OAI.TamingCompatibility.ExteriorForms.wedgeOne_comp line 72
  10. lemma OAI.TamingCompatibility.ExteriorForms.oneLinear_comp line 79
  11. lemma OAI.TamingCompatibility.ExteriorForms.wedgeOne_contDiffOn line 84
  12. lemma OAI.TamingCompatibility.ExteriorForms.extDeriv_one line 96
  13. lemma OAI.TamingCompatibility.ExteriorForms.extDeriv_two line 103
  14. lemma OAI.TamingCompatibility.ExteriorForms.extDeriv_three line 113
  15. lemma OAI.TamingCompatibility.ExteriorForms.fderiv_eval line 124
  16. def OAI.TamingCompatibility.ExteriorForms.wedgeOneBilinear line 130
  17. lemma OAI.TamingCompatibility.ExteriorForms.wedgeOneBilinear_apply line 136
  18. lemma OAI.TamingCompatibility.ExteriorForms.fderiv_wedgeOne line 139
  19. lemma OAI.TamingCompatibility.ExteriorForms.extDeriv_wedgeOne line 147