OAI/Analysis/CircleDomains/Rigidity/AffineTracePairs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Affine changes of the two scalar coordinates preserve outer-null trace pairs, including singular changes with one constant coordinate.

  1. theorem OAI.CircleDomainRigidity.affine_pair_image_null line 13
  2. theorem OAI.CircleDomainRigidity.affine_trace_pair_null line 35