OAI/Geometry/WeakMTW/Potentials/PotentialActiveLogs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WeakMTWGlobalSupport.WeakMTW.cTransform_continuous line 22
  2. theorem OAI.WeakMTWGlobalSupport.WeakMTW.cTransform_ge line 28
  3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.cTransform_attained line 35
  4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.isPotential_continuous line 44
  5. def OAI.WeakMTWGlobalSupport.WeakMTW.potentialActive line 48
  6. def OAI.WeakMTWGlobalSupport.WeakMTW.potentialActiveGraph line 50
  7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.potentialActive_nonempty line 53
  8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.potentialActiveGraph_compact line 63
  9. theorem OAI.WeakMTWGlobalSupport.WeakMTW.potentialActive_subseq line 71
  10. theorem OAI.WeakMTWGlobalSupport.WeakMTW.potentialActive_shortened_support line 86
  11. theorem OAI.WeakMTWGlobalSupport.WeakMTW.potentialActiveHull_closed line 96