OAI/Analysis/JiangSu/Absorption/OneSidedIntertwiningChain2.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NonunitalIntertwining.error line 19
  2. lemma OAI.NonunitalIntertwining.error_pos line 20
  3. lemma OAI.NonunitalIntertwining.error_tendsto line 21
  4. lemma OAI.NonunitalIntertwining.error_add line 23
  5. lemma OAI.NonunitalIntertwining.controlled_cauchy line 25
  6. lemma OAI.NonunitalIntertwining.controlled_limit_distance line 34
  7. theorem OAI.NonunitalIntertwining.equiv_of_chain line 48
  8. def OAI.NonunitalIntertwining.LocalApproximation line 91
  9. structure OAI.NonunitalIntertwining.ProtectedEmbedding line 97
  10. def OAI.NonunitalIntertwining.ProtectedEmbedding.hom line 101
  11. def OAI.NonunitalIntertwining.Transition line 104
  12. lemma OAI.NonunitalIntertwining.transition_exists line 110
  13. theorem OAI.NonunitalIntertwining.equiv_of_local_approximation line 136
  14. lemma OAI.NonunitalIntertwining.norm_eventually_lt line 172
  15. def OAI.NonunitalIntertwining.AmbientQuotientConjugacy line 178
  16. theorem OAI.NonunitalIntertwining.local_approximation_of_ambient_quotient line 190
  17. theorem OAI.NonunitalIntertwining.equiv_of_ambient_quotient_conjugacy line 243