OAI/Geometry/TamingCompatibility/Charts/UnitaryFrames.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.LocalUnitaryFrame.Bilinear line 27
  2. lemma OAI.TamingCompatibility.LocalUnitaryFrame.skew line 30
  3. lemma OAI.TamingCompatibility.LocalUnitaryFrame.orthogonal_J line 37
  4. def OAI.TamingCompatibility.LocalUnitaryFrame.normalize line 45
  5. lemma OAI.TamingCompatibility.LocalUnitaryFrame.normalize_unit line 47
  6. lemma OAI.TamingCompatibility.LocalUnitaryFrame.normalize_eq_of_unit line 55
  7. def OAI.TamingCompatibility.LocalUnitaryFrame.transverse line 58
  8. lemma OAI.TamingCompatibility.LocalUnitaryFrame.transverse_orthogonal line 61
  9. lemma OAI.TamingCompatibility.LocalUnitaryFrame.transverse_eq line 71
  10. def OAI.TamingCompatibility.LocalUnitaryFrame.frame line 75
  11. lemma OAI.TamingCompatibility.LocalUnitaryFrame.frame_gram line 77
  12. lemma OAI.TamingCompatibility.LocalUnitaryFrame.contDiffOn_evaluate line 99
  13. lemma OAI.TamingCompatibility.LocalUnitaryFrame.contDiffOn_normalize line 103
  14. lemma OAI.TamingCompatibility.LocalUnitaryFrame.contDiffOn_transverse line 112
  15. lemma OAI.TamingCompatibility.LocalUnitaryFrame.exists_smooth_frame_near line 118