OAI/NumberTheory/Ostmann/Endpoint.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.finite_symmDiff_iff_eventuallyEqual line 8
  2. theorem OAI.Ostmann.infinite_symmDiff_iff_not_eventuallyEqual line 30
  3. theorem OAI.Ostmann.EventuallyEqual.refl line 34
  4. theorem OAI.Ostmann.EventuallyEqual.symm line 37
  5. theorem OAI.Ostmann.EventuallyEqual.trans line 42
  6. theorem OAI.Ostmann.eventual_sumset_iff line 49
  7. theorem OAI.Ostmann.indecomposable_iff_no_eventual_decomposition line 68
  8. theorem OAI.Ostmann.indecomposable_iff_finite_modifications line 77
  9. theorem OAI.Ostmann.finite_set_infinite_prime_disagreement line 87
  10. theorem OAI.Ostmann.finite_finite_disagreement line 93
  11. theorem OAI.Ostmann.eventual_decomposition_infinite_or line 96
  12. theorem OAI.Ostmann.nontrivial_iff_exists_lt line 106
  13. theorem OAI.Ostmann.assemble_indecomposability line 116
  14. theorem OAI.Ostmann.countUpTo_mono_set line 130
  15. theorem OAI.Ostmann.countUpTo_sumset_le line 137
  16. theorem OAI.Ostmann.countUpTo_le_of_eventual_cutoff line 151
  17. theorem OAI.Ostmann.EventuallyEqual.counting_bounds line 165
  18. theorem OAI.Ostmann.countUpTo_primes line 172
  19. theorem OAI.Ostmann.EventuallyEqual.primeCounting_le line 179