OAI/Analysis/JiangSu/CentralSequences/NormUltrapowerBasic.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.NormUltra.BoundedFamilies line 13
  2. lemma OAI.NormUltra.BoundedFamilies.norm_coordinate_le line 16
  3. def OAI.NormUltra.BoundedFamilies.vanishing line 19
  4. lemma OAI.NormUltra.BoundedFamilies.mem_vanishing line 29
  5. lemma OAI.NormUltra.BoundedFamilies.mul_mem_vanishing_left line 32
  6. lemma OAI.NormUltra.BoundedFamilies.mul_mem_vanishing_right line 41
  7. lemma OAI.NormUltra.BoundedFamilies.star_mem_vanishing line 50
  8. instance OAI.NormUltra.BoundedFamilies.vanishing_closed line 54
  9. def OAI.NormUltra.BoundedFamilies.vanishingCon line 71
  10. def OAI.NormUltra.QuotientAlgebra line 91
  11. instance OAI.NormUltra.QuotientAlgebra.(instance at line 96) line 96
  12. instance OAI.NormUltra.QuotientAlgebra.(instance at line 98) line 98
  13. instance OAI.NormUltra.QuotientAlgebra.(instance at line 100) line 100
  14. instance OAI.NormUltra.QuotientAlgebra.(instance at line 102) line 102
  15. instance OAI.NormUltra.QuotientAlgebra.(instance at line 104) line 104
  16. def OAI.NormUltra.QuotientAlgebra.mk line 107
  17. lemma OAI.NormUltra.QuotientAlgebra.mk_add line 108
  18. lemma OAI.NormUltra.QuotientAlgebra.mk_mul line 109
  19. lemma OAI.NormUltra.QuotientAlgebra.mk_sub line 110
  20. lemma OAI.NormUltra.QuotientAlgebra.mk_smul line 111
  21. lemma OAI.NormUltra.QuotientAlgebra.mk_zero line 112
  22. lemma OAI.NormUltra.QuotientAlgebra.mk_surjective line 113
  23. lemma OAI.NormUltra.QuotientAlgebra.mk_eq_mk_iff line 114
  24. lemma OAI.NormUltra.QuotientAlgebra.norm_mk_le line 116
  25. lemma OAI.NormUltra.QuotientAlgebra.exists_norm_mk_lt line 117
  26. instance OAI.NormUltra.QuotientAlgebra.(instance at line 120) line 120
  27. instance OAI.NormUltra.QuotientAlgebra.(instance at line 134) line 134
  28. lemma OAI.NormUltra.QuotientAlgebra.mk_star line 140
  29. instance OAI.NormUltra.QuotientAlgebra.(instance at line 141) line 141
  30. instance OAI.NormUltra.QuotientAlgebra.(instance at line 156) line 156
  31. instance OAI.NormUltra.QuotientAlgebra.(instance at line 161) line 161
  32. instance OAI.NormUltra.QuotientAlgebra.(instance at line 167) line 167
  33. lemma OAI.NormUltra.BoundedFamilies.norm_bounded line 186
  34. lemma OAI.NormUltra.BoundedFamilies.norm_cobounded line 189
  35. lemma OAI.NormUltra.BoundedFamilies.limsup_norm_nonneg line 193
  36. lemma OAI.NormUltra.BoundedFamilies.limsup_norm_le_of_vanishing_sub line 197
  37. def OAI.NormUltra.BoundedFamilies.mask line 210
  38. lemma OAI.NormUltra.BoundedFamilies.mask_sub_mem line 218
  39. lemma OAI.NormUltra.BoundedFamilies.norm_mask_le line 225
  40. theorem OAI.NormUltra.QuotientAlgebra.norm_mk_eq_limsup line 238
  41. lemma OAI.NormUltra.QuotientAlgebra.norm_star_mul_self_eq line 257
  42. instance OAI.NormUltra.QuotientAlgebra.(instance at line 275) line 275
  43. instance OAI.NormUltra.QuotientAlgebra.(instance at line 277) line 277
  44. def OAI.NormUltra.QuotientAlgebra.mkHom line 279