OAI/Geometry/PrescribedRicci/FiniteCofactorPatch.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite Cofactor Patch.

  1. def OAI.GlobalElliptic.GluingData.cofactorLocal line 26
  2. lemma OAI.GlobalElliptic.GluingData.cofactorLocal_continuous line 36
  3. lemma OAI.GlobalElliptic.GluingData.cofactorLocal_zero line 41
  4. def OAI.GlobalElliptic.GluingData.cofactorBCF line 46
  5. lemma OAI.GlobalElliptic.GluingData.cofactorBCF_continuous line 51
  6. lemma OAI.GlobalElliptic.GluingData.cofactorBCF_zero line 60
  7. lemma OAI.GlobalElliptic.GluingData.cofactorBCF_lower line 67
  8. def OAI.GlobalElliptic.GluingData.CofactorSmall line 89
  9. lemma OAI.GlobalElliptic.GluingData.cofactor_small_nhds line 96
  10. lemma OAI.GlobalElliptic.GluingData.cofactor_small_of_lower line 112