OAI/Analysis/IrrationalRotation/Operators/AffiliatedTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InvariantRotation.AffiliatedTransport.mem_domainImage line 14
  2. theorem OAI.InvariantRotation.AffiliatedTransport.domainImage_invariant line 18
  3. theorem OAI.InvariantRotation.AffiliatedTransport.transported_invariant line 29
  4. theorem OAI.InvariantRotation.AffiliatedTransport.transported_invariant_of_commutes line 41
  5. theorem OAI.InvariantRotation.AffiliatedTransport.mem_transported_orthogonal line 49
  6. theorem OAI.InvariantRotation.AffiliatedTransport.inverse_domainImage_le_orthogonal line 59
  7. theorem OAI.InvariantRotation.AffiliatedTransport.inverse_transported_le_orthogonal line 75
  8. theorem OAI.InvariantRotation.AffiliatedTransport.inverse_transported_le_orthogonal_of_selfAdjoint line 87
  9. theorem OAI.InvariantRotation.AffiliatedTransport.transported_projection_mem line 100