OAI/Analysis/CircleDomains/Topology/PlanarAxisSwap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Interchanging physical coordinate axes preserves area and exchanges horizontal and vertical fiber tests.

  1. def OAI.CircleDomainRigidity.planarAxisSwap line 14
  2. theorem OAI.CircleDomainRigidity.continuous_planarAxisSwap line 16
  3. theorem OAI.CircleDomainRigidity.planarAxisSwap_involutive line 20
  4. theorem OAI.CircleDomainRigidity.planarAxisSwap_bijective line 22
  5. theorem OAI.CircleDomainRigidity.planarAxisSwap_measurePreserving line 25
  6. theorem OAI.CircleDomainRigidity.planarAxisSwap_preimage_box line 32
  7. theorem OAI.CircleDomainRigidity.planarAxisSwap_image_box line 38
  8. theorem OAI.CircleDomainRigidity.planarAxisSwap_image_horizontal_fiber line 47
  9. theorem OAI.CircleDomainRigidity.lintegral_planarAxisSwap_box line 57