OAI/Analysis/JiangSu/Nonunital/FiniteTraceIdeal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NonunitalGamma.star_square_add_le line 16
  2. lemma OAI.NonunitalGamma.finite_star_square_add line 25
  3. lemma OAI.NonunitalGamma.finite_star_square_mul_left line 36
  4. lemma OAI.NonunitalGamma.finite_star_square_mul_right line 47
  5. def OAI.NonunitalGamma.finiteTraceIdeal line 58
  6. lemma OAI.NonunitalGamma.mem_finiteTraceIdeal line 69
  7. lemma OAI.NonunitalGamma.finiteTraceIdeal_dense line 73
  8. theorem OAI.NonunitalGamma.denselyFinite_of_finite_nonzero line 100
  9. lemma OAI.NonunitalGamma.bounded_ray_of_finite_test line 120
  10. def OAI.NonunitalGamma.generalizedLimitValue line 147
  11. lemma OAI.NonunitalGamma.ennreal_ultrafilter_tendsto line 151
  12. lemma OAI.NonunitalGamma.cut_nonzero_exists line 157
  13. lemma OAI.NonunitalGamma.eventually_finite_test line 170
  14. theorem OAI.NonunitalGamma.generalized_eventually_bounded_rays line 182