OAI/Combinatorics/PolynomialVacuum/Bridge/FiniteOpenPath.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumOpenPath.follow line 9
  2. theorem OAI.PolynomialVacuumOpenPath.follow_zero line 13
  3. theorem OAI.PolynomialVacuumOpenPath.follow_succ line 14
  4. theorem OAI.PolynomialVacuumOpenPath.follow_injective line 18
  5. theorem OAI.PolynomialVacuumOpenPath.eventually_exits line 54
  6. def OAI.PolynomialVacuumOpenPath.exitTime line 76
  7. theorem OAI.PolynomialVacuumOpenPath.exitTime_spec line 78
  8. theorem OAI.PolynomialVacuumOpenPath.exitTime_pos line 81
  9. theorem OAI.PolynomialVacuumOpenPath.beforeExit_some line 87
  10. def OAI.PolynomialVacuumOpenPath.pathAt line 91
  11. theorem OAI.PolynomialVacuumOpenPath.pathAt_spec line 94
  12. theorem OAI.PolynomialVacuumOpenPath.pathAt_injective line 98
  13. theorem OAI.PolynomialVacuumOpenPath.pathAt_start line 105
  14. theorem OAI.PolynomialVacuumOpenPath.pathAt_next line 108
  15. theorem OAI.PolynomialVacuumOpenPath.pathAt_exit line 114