OAI/Geometry/TamingCompatibility/DifferentialForms/UnitaryFrame.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.UnitaryFrame.V line 23
  2. abbrev OAI.TamingCompatibility.UnitaryFrame.W line 24
  3. def OAI.TamingCompatibility.UnitaryFrame.J line 26
  4. def OAI.TamingCompatibility.UnitaryFrame.wedge line 28
  5. def OAI.TamingCompatibility.UnitaryFrame.star line 33
  6. def OAI.TamingCompatibility.UnitaryFrame.fundamental line 35
  7. def OAI.TamingCompatibility.UnitaryFrame.line line 37
  8. def OAI.TamingCompatibility.UnitaryFrame.selfDualPart line 39
  9. lemma OAI.TamingCompatibility.UnitaryFrame.J_square line 41
  10. lemma OAI.TamingCompatibility.UnitaryFrame.star_square line 45
  11. lemma OAI.TamingCompatibility.UnitaryFrame.star_add line 49
  12. lemma OAI.TamingCompatibility.UnitaryFrame.star_smul line 53
  13. lemma OAI.TamingCompatibility.UnitaryFrame.star_self_adjoint line 57
  14. lemma OAI.TamingCompatibility.UnitaryFrame.star_isometry line 61
  15. lemma OAI.TamingCompatibility.UnitaryFrame.J_inner line 64
  16. lemma OAI.TamingCompatibility.UnitaryFrame.inner_self_J line 68
  17. lemma OAI.TamingCompatibility.UnitaryFrame.wedge_inner line 72
  18. lemma OAI.TamingCompatibility.UnitaryFrame.star_fundamental line 77
  19. lemma OAI.TamingCompatibility.UnitaryFrame.fundamental_norm_sq line 81
  20. lemma OAI.TamingCompatibility.UnitaryFrame.line_selfDualPart line 84
  21. lemma OAI.TamingCompatibility.UnitaryFrame.line_norm_sq line 92
  22. lemma OAI.TamingCompatibility.UnitaryFrame.fundamental_eval_line line 97
  23. lemma OAI.TamingCompatibility.UnitaryFrame.unit_line_norm line 103
  24. lemma OAI.TamingCompatibility.UnitaryFrame.unit_line_selfDualPart line 108
  25. theorem OAI.TamingCompatibility.UnitaryFrame.angular_identity line 113
  26. def OAI.TamingCompatibility.UnitaryFrame.jAction line 129
  27. def OAI.TamingCompatibility.UnitaryFrame.antiInvariantPart line 131
  28. lemma OAI.TamingCompatibility.UnitaryFrame.jAction_square line 133
  29. lemma OAI.TamingCompatibility.UnitaryFrame.star_antiInvariantPart line 137
  30. lemma OAI.TamingCompatibility.UnitaryFrame.antiInvariantPart_fundamental line 141
  31. def OAI.TamingCompatibility.UnitaryFrame.interior line 145
  32. theorem OAI.TamingCompatibility.UnitaryFrame.closed_lift_principal_symbol line 151