OAI/Analysis/MarkovType/ScalarUltralimit.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.RealSeqBounded line 15
  2. theorem OAI.MarkovSuperreflexivity.RealSeqBounded.exists_nonneg_bound line 22
  3. theorem OAI.MarkovSuperreflexivity.RealSeqBounded.const line 27
  4. theorem OAI.MarkovSuperreflexivity.RealSeqBounded.add line 30
  5. theorem OAI.MarkovSuperreflexivity.RealSeqBounded.neg line 36
  6. theorem OAI.MarkovSuperreflexivity.RealSeqBounded.sub line 41
  7. theorem OAI.MarkovSuperreflexivity.RealSeqBounded.const_mul line 45
  8. theorem OAI.MarkovSuperreflexivity.RealSeqBounded.abs line 52
  9. def OAI.MarkovSuperreflexivity.realULim line 59
  10. theorem OAI.MarkovSuperreflexivity.tendsto_realULim line 64
  11. theorem OAI.MarkovSuperreflexivity.realULim_eq_of_tendsto line 75
  12. theorem OAI.MarkovSuperreflexivity.realULim_const line 80
  13. theorem OAI.MarkovSuperreflexivity.realULim_add line 84
  14. theorem OAI.MarkovSuperreflexivity.realULim_neg line 89
  15. theorem OAI.MarkovSuperreflexivity.realULim_sub line 93
  16. theorem OAI.MarkovSuperreflexivity.realULim_const_mul line 98
  17. theorem OAI.MarkovSuperreflexivity.realULim_abs line 102
  18. theorem OAI.MarkovSuperreflexivity.realULim_le_realULim line 106
  19. theorem OAI.MarkovSuperreflexivity.realULim_le_of_eventually_le line 111
  20. theorem OAI.MarkovSuperreflexivity.le_realULim_of_eventually_le line 115
  21. def OAI.MarkovSuperreflexivity.freeUltrafilter line 120
  22. theorem OAI.MarkovSuperreflexivity.freeUltrafilter_le_cofinite line 122
  23. theorem OAI.MarkovSuperreflexivity.freeUltrafilter_le_atTop line 126
  24. theorem OAI.MarkovSuperreflexivity.not_mem_freeUltrafilter_of_finite line 129
  25. theorem OAI.MarkovSuperreflexivity.tendsto_freeUltrafilter_of_tendsto_atTop line 133
  26. theorem OAI.MarkovSuperreflexivity.realULim_freeUltrafilter_eq_of_tendsto_atTop line 138