OAI/Analysis/CircleDomains/Sobolev/LipschitzIntervalPaths.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Concrete paths obtained by traversing a real interval in a Lipschitz chart.

  1. def OAI.CircleDomainRigidity.realIntervalPath line 15
  2. theorem OAI.CircleDomainRigidity.realIntervalPath_zero line 19
  3. theorem OAI.CircleDomainRigidity.realIntervalPath_one line 22
  4. theorem OAI.CircleDomainRigidity.realIntervalPath_lipschitz line 25
  5. theorem OAI.CircleDomainRigidity.realIntervalPath_antilipschitz line 32
  6. theorem OAI.CircleDomainRigidity.realIntervalPath_mem line 41
  7. theorem OAI.CircleDomainRigidity.range_realIntervalPath line 48
  8. theorem OAI.CircleDomainRigidity.lipschitz_path_boundedVariation line 64
  9. theorem OAI.CircleDomainRigidity.intervalChart_lipschitz line 75
  10. def OAI.CircleDomainRigidity.intervalChartPath line 89
  11. theorem OAI.CircleDomainRigidity.intervalChartPath_lipschitz line 94