OAI/Geometry/TamingCompatibility/Functional/PlaneNormalization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.PlaneVariation.first line 13
  2. def OAI.TamingCompatibility.PlaneVariation.normalPart line 15
  3. def OAI.TamingCompatibility.PlaneVariation.second line 17
  4. def OAI.TamingCompatibility.PlaneVariation.area line 19
  5. lemma OAI.TamingCompatibility.PlaneVariation.norm_first line 21
  6. lemma OAI.TamingCompatibility.PlaneVariation.first_reconstruct line 25
  7. lemma OAI.TamingCompatibility.PlaneVariation.normalPart_orthogonal line 30
  8. lemma OAI.TamingCompatibility.PlaneVariation.norm_second line 34
  9. lemma OAI.TamingCompatibility.PlaneVariation.first_second_orthogonal line 37
  10. lemma OAI.TamingCompatibility.PlaneVariation.second_reconstruct line 40
  11. lemma OAI.TamingCompatibility.PlaneVariation.normalPart_complex_ne_zero line 43
  12. lemma OAI.TamingCompatibility.PlaneVariation.area_pos line 58
  13. lemma OAI.TamingCompatibility.PlaneVariation.reconstruct_second line 61
  14. lemma OAI.TamingCompatibility.PlaneVariation.alternating_area line 66
  15. lemma OAI.TamingCompatibility.PlaneVariation.first_continuousAt line 80
  16. lemma OAI.TamingCompatibility.PlaneVariation.normalPart_continuousAt line 83
  17. lemma OAI.TamingCompatibility.PlaneVariation.second_continuousAt line 91
  18. lemma OAI.TamingCompatibility.PlaneVariation.area_continuousAt line 98