OAI/Geometry/PrescribedPotential/PatchCutoffs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Patch Cutoffs.

  1. theorem OAI.GlobalElliptic.exists_chartCutoff line 24
  2. structure OAI.GlobalElliptic.GluingData line 49
  3. theorem OAI.GlobalElliptic.exists_gluingData line 61
  4. lemma OAI.GlobalElliptic.GluingData.exists_outerCutoff line 89
  5. def OAI.GlobalElliptic.GluingData.outerCutoff line 99
  6. lemma OAI.GlobalElliptic.GluingData.outerCutoff_support line 102
  7. lemma OAI.GlobalElliptic.GluingData.outerCutoff_one line 106