OAI/Geometry/PolarProducts/MoserFlow.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothODE.fiberHomeomorph line 30
  2. theorem OAI.SmoothODE.fiberHomeomorph_apply line 58
  3. theorem OAI.SmoothODE.fiberHomeomorph_symm_apply line 63
  4. theorem OAI.SmoothODE.contDiff_fiberHomeomorph line 67
  5. theorem OAI.SmoothODE.contDiff_fiberHomeomorph_symm line 73
  6. theorem OAI.SmoothODE.fderiv_fiberHomeomorph line 79
  7. theorem OAI.SmoothODE.fiberHomeomorph_mapsTo line 105
  8. theorem OAI.Moser.compactlySupported_deformation line 135