OAI/Analysis/WeakInfiniteness/SeparationScalar.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.separationFloor line 23
  2. def OAI.WeakPureInfiniteness.separationR line 25
  3. def OAI.WeakPureInfiniteness.separationV line 27
  4. def OAI.WeakPureInfiniteness.separationK line 29
  5. def OAI.WeakPureInfiniteness.separationG line 31
  6. def OAI.WeakPureInfiniteness.separationN line 33
  7. def OAI.WeakPureInfiniteness.separationL line 35
  8. lemma OAI.WeakPureInfiniteness.separationFloor_pos line 37
  9. lemma OAI.WeakPureInfiniteness.continuous_separationFloor line 40
  10. lemma OAI.WeakPureInfiniteness.continuous_separationR line 43
  11. lemma OAI.WeakPureInfiniteness.continuous_separationV line 48
  12. lemma OAI.WeakPureInfiniteness.continuous_separationK line 53
  13. lemma OAI.WeakPureInfiniteness.continuous_separationG line 58
  14. lemma OAI.WeakPureInfiniteness.continuous_separationN line 61
  15. lemma OAI.WeakPureInfiniteness.continuous_separationL line 64
  16. lemma OAI.WeakPureInfiniteness.separationR_nonneg line 67
  17. lemma OAI.WeakPureInfiniteness.separationV_nonneg line 70
  18. lemma OAI.WeakPureInfiniteness.separationR_sq line 73
  19. lemma OAI.WeakPureInfiniteness.separationV_sq line 77
  20. lemma OAI.WeakPureInfiniteness.separationR_le_one line 82
  21. lemma OAI.WeakPureInfiniteness.separation_floor_ge_sqrt line 86
  22. lemma OAI.WeakPureInfiniteness.separation_floor_eq line 88
  23. lemma OAI.WeakPureInfiniteness.separation_sV_sq_le_one line 91
  24. lemma OAI.WeakPureInfiniteness.separationG_zero line 104
  25. lemma OAI.WeakPureInfiniteness.separationN_zero line 107
  26. lemma OAI.WeakPureInfiniteness.separationGN line 110
  27. lemma OAI.WeakPureInfiniteness.separationVRG line 116
  28. lemma OAI.WeakPureInfiniteness.separation_low_support line 131
  29. lemma OAI.WeakPureInfiniteness.separationL_bounds line 136