OAI/Geometry/TamingCompatibility/DifferentialForms/Sign.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.OrientationSign.sign line 29
  2. lemma OAI.TamingCompatibility.OrientationSign.abs_mul_div line 31
  3. lemma OAI.TamingCompatibility.OrientationSign.locally_constant line 40
  4. lemma OAI.TamingCompatibility.OrientationSign.contDiffOn line 51
  5. lemma OAI.TamingCompatibility.OrientationSign.extDeriv_smul line 57
  6. lemma OAI.TamingCompatibility.ExteriorForms.volumeSquare_contDiffOn line 73
  7. def OAI.TamingCompatibility.ManifoldTop.basisIndex line 91
  8. def OAI.TamingCompatibility.ManifoldTop.basis line 92
  9. lemma OAI.TamingCompatibility.ManifoldTop.density_basis line 94
  10. def OAI.TamingCompatibility.ManifoldTop.volumeForm line 105
  11. lemma OAI.TamingCompatibility.ManifoldTop.pullback_volumeForm line 108
  12. lemma OAI.TamingCompatibility.ManifoldTop.volumeForm_smooth line 113
  13. lemma OAI.TamingCompatibility.ManifoldTop.volumeForm_ne_zero line 123
  14. def OAI.TamingCompatibility.ManifoldTop.coefficient line 134
  15. lemma OAI.TamingCompatibility.ManifoldTop.coefficient_chart line 137
  16. lemma OAI.TamingCompatibility.ManifoldTop.coordinateVolume_ne_zero line 148
  17. lemma OAI.TamingCompatibility.ManifoldTop.scalar_smooth_of_charts line 158
  18. lemma OAI.TamingCompatibility.ManifoldTop.coefficient_smooth line 170
  19. lemma OAI.TamingCompatibility.ManifoldTop.coordinateFundamental line 183
  20. lemma OAI.TamingCompatibility.ManifoldTop.abs_coordinateVolume line 198
  21. lemma OAI.TamingCompatibility.ManifoldTop.density_coefficient line 210