OAI/Analysis/CircleDomains/Topology/PlanarFormPullback.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual exterior derivative of a pulled-back smooth planar one-form. This is a calculus identity used in the construction of Green's formula.

  1. def OAI.CircleDomainRigidity.pulledPlanarForm line 14
  2. lemma OAI.CircleDomainRigidity.pulledPlanarForm_contDiff line 19
  3. lemma OAI.CircleDomainRigidity.pulledPlanarForm_fderiv line 27
  4. lemma OAI.CircleDomainRigidity.pulledPlanarForm_curl line 55