OAI/Geometry/BallPacking/Necessity/CompactContinuation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TwoPointContinuation.finite_space_continuation line 39
  2. theorem OAI.TwoPointContinuation.compact_residual_gap line 78
  3. theorem OAI.TwoPointContinuation.compact_continuation line 111
  4. theorem OAI.TwoPointContinuation.local_compact_continuation line 196
  5. def OAI.TwoPointContinuation.LocallyPrecompact line 276
  6. theorem OAI.TwoPointContinuation.locallyPrecompact_finite line 279
  7. theorem OAI.TwoPointContinuation.locallyPrecompact_compactLinear line 285
  8. theorem OAI.TwoPointContinuation.LocallyPrecompact.prod line 297
  9. theorem OAI.TwoPointContinuation.LocallyPrecompact.comp line 305
  10. theorem OAI.TwoPointContinuation.compact_tube_precompact line 322
  11. theorem OAI.TwoPointContinuation.local_degree_continuation line 353