OAI/Analysis/CircleDomains/Topology/CompactPlanarCurl.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The integral of a compactly supported smooth derivative, and hence of its planar curl, vanishes on the whole plane.

  1. lemma OAI.CircleDomainRigidity.integral_compact_fderiv_eq_zero line 14
  2. lemma OAI.CircleDomainRigidity.integral_compact_planar_curl line 31