OAI/Geometry/WeakMTW/Support/FiniteActiveGraph.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakMTWGlobalSupport.WeakMTW.finitePotential line 22
  2. def OAI.WeakMTWGlobalSupport.WeakMTW.activeVelocities line 25
  3. def OAI.WeakMTWGlobalSupport.WeakMTW.activeHull line 28
  4. def OAI.WeakMTWGlobalSupport.WeakMTW.activeGraph line 31
  5. def OAI.WeakMTWGlobalSupport.WeakMTW.activeHullGraph line 34
  6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.cost_continuous line 38
  7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.finitePotential_continuous line 42
  8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.finitePotential_ge line 48
  9. theorem OAI.WeakMTWGlobalSupport.WeakMTW.finitePotential_attained line 53
  10. theorem OAI.WeakMTWGlobalSupport.WeakMTW.activeVelocities_nonempty line 58
  11. theorem OAI.WeakMTWGlobalSupport.WeakMTW.activeGraph_eq line 69
  12. theorem OAI.WeakMTWGlobalSupport.WeakMTW.activeGraph_compact line 76
  13. theorem OAI.WeakMTWGlobalSupport.WeakMTW.activeHull_bound line 91