OAI/Analysis/CircleDomains/Rigidity/AxialSwapDisks.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The coordinate swap preserves the actual closed disk family.

  1. theorem OAI.CircleDomainRigidity.axialSwap_involutive line 10
  2. theorem OAI.CircleDomainRigidity.axialSwap_mem_closedBall_iff line 14
  3. theorem OAI.CircleDomainRigidity.axialSwap_pairwise_disjoint line 18
  4. theorem OAI.CircleDomainRigidity.horizontal_mem_swapped_disk line 32