OAI/Geometry/PrescribedPotential/RealVolume.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Real Volume.

  1. lemma OAI.RealClosedDerivative.subtype_iff line 21
  2. def OAI.GlobalElliptic.GluingData.realVolume line 46
  3. lemma OAI.GlobalElliptic.GluingData.realVolume_continuous line 50
  4. lemma OAI.GlobalElliptic.GluingData.realVolume_ambient_contDiff line 54
  5. lemma OAI.GlobalElliptic.GluingData.completedVolume_real_directional line 58
  6. lemma OAI.GlobalElliptic.GluingData.realVolume_hasStrictFDerivAt_zero line 83
  7. lemma OAI.GlobalElliptic.GluingData.realVolume_zero line 116