OAI/Analysis/SymmetricDomains/CayleyTangentBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.graphConormal line 36
  2. theorem OAI.Release061.graphConormal_surjective line 58
  3. theorem OAI.Release061.graphConormal_injective line 75
  4. def OAI.Release061.normalCayley line 88
  5. def OAI.Release061.normalUncayley line 89
  6. lemma OAI.Release061.add_I_ne_zero_of_im_pos line 91
  7. lemma OAI.Release061.one_sub_ne_zero_of_norm_lt_one line 97
  8. lemma OAI.Release061.normalCayley_sub_one line 102
  9. lemma OAI.Release061.normalCayley_ne_one line 108
  10. lemma OAI.Release061.normalUncayley_add_I line 114
  11. lemma OAI.Release061.normalUncayley_add_I_ne_zero line 120
  12. lemma OAI.Release061.normalUncayley_cayley line 125
  13. lemma OAI.Release061.normalCayley_uncayley line 131
  14. lemma OAI.Release061.norm_normalCayley_lt_one line 137
  15. lemma OAI.Release061.one_add_im_le_norm_add_I line 145
  16. lemma OAI.Release061.cayley_tangent_bound line 150