OAI/Analysis/CharacterCriterion/NormUltrapower.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KirchbergRordam.NormUltrapower.exists_norm_limit line 36
  2. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_nonneg line 45
  3. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_le line 48
  4. theorem OAI.KirchbergRordam.NormUltrapower.tendsto_norm line 51
  5. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_zero line 56
  6. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_neg line 61
  7. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_add_le line 66
  8. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_mul_le line 72
  9. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_star line 79
  10. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_star_mul line 84
  11. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_sub_le line 90
  12. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_lipschitz line 96
  13. theorem OAI.KirchbergRordam.NormUltrapower.mem_nullIdeal line 109
  14. theorem OAI.KirchbergRordam.NormUltrapower.star_mk line 119
  15. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_eq_of_sub_mem line 123
  16. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_le_quotient line 134
  17. theorem OAI.KirchbergRordam.NormUltrapower.cutRepresentative_norm_le line 143
  18. theorem OAI.KirchbergRordam.NormUltrapower.cutRepresentative_mk_eq line 152
  19. theorem OAI.KirchbergRordam.NormUltrapower.quotient_norm_le_normLimit line 166
  20. theorem OAI.KirchbergRordam.NormUltrapower.norm_mk_eq line 177
  21. theorem OAI.KirchbergRordam.NormUltrapower.normLimit_const line 182
  22. theorem OAI.KirchbergRordam.NormUltrapower.norm_diagonal line 187
  23. theorem OAI.KirchbergRordam.NormUltrapower.diagonal_isometry line 191
  24. instance OAI.KirchbergRordam.NormUltrapower.quotientNontrivial line 196
  25. instance OAI.KirchbergRordam.NormUltrapower.centralNontrivial line 200
  26. theorem OAI.KirchbergRordam.NormUltrapower.mem_central_iff line 203
  27. theorem OAI.KirchbergRordam.NormUltrapower.mk_mem_central_iff line 215