OAI/Analysis/SymmetricDomains/EventualOffsetBall.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.offsetScaled line 31
  2. def OAI.Release061.offsetDistance line 34
  3. lemma OAI.Release061.offsetDistance_nonneg line 38
  4. lemma OAI.Release061.offsetDistance_le_one line 42
  5. lemma OAI.Release061.offsetDistance_lipschitz line 45
  6. lemma OAI.Release061.offset_excluded_nonempty line 51
  7. lemma OAI.Release061.offsetDistance_zero line 55
  8. lemma OAI.Release061.ball_subset_offsetScaled line 61
  9. lemma OAI.Release061.radius_le_infDist_compl line 73
  10. theorem OAI.Release061.excluded_offset_noncollapse line 81
  11. lemma OAI.Release061.complex_ball_offset_ball line 112
  12. lemma OAI.Release061.tendsto_of_truncated_zero line 127
  13. lemma OAI.Release061.moving_offsetDistance_limit line 136
  14. lemma OAI.Release061.excluded_limit_from_offsetDistance line 147
  15. lemma OAI.Release061.eventual_offset_ball line 154