OAI/Analysis/CircleDomains/Rigidity/SphereTracePairNull.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact trace-pair transfer between the finite plane and a sphere complement avoiding infinity.

  1. theorem OAI.CircleDomainRigidity.sphere_trace_pair_null_of_plane line 13
  2. theorem OAI.CircleDomainRigidity.plane_trace_pair_null_of_sphere line 25
  3. theorem OAI.CircleDomainRigidity.sphereFromPlaneFunction_flatten line 31