OAI/Analysis/CircleDomains/Rigidity/AxialChordGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Both source-axis geometries use the same exact real chord intervals. Swapping real coordinates preserves every source disk and its distances.

  1. def OAI.CircleDomainRigidity.axialSwap line 13
  2. theorem OAI.CircleDomainRigidity.axialSwap_dist line 15
  3. theorem OAI.CircleDomainRigidity.axialSwap_line line 22
  4. theorem OAI.CircleDomainRigidity.axialSwap_im line 27
  5. def OAI.CircleDomainRigidity.axialChord line 30
  6. theorem OAI.CircleDomainRigidity.mem_closedBall_iff_mem_axialChord line 32
  7. theorem OAI.CircleDomainRigidity.axial_ball_preimage_ordConnected line 42