OAI/Analysis/CircleDomains/Rigidity/LipschitzTracePairs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Coordinatewise scalar Lipschitz changes preserve null planar trace pairs, including the constructed countable-value flattenings.

  1. theorem OAI.CircleDomainRigidity.lipschitz_plane_image_null line 13
  2. theorem OAI.CircleDomainRigidity.coordinate_lipschitz_pair_null line 19
  3. theorem OAI.CircleDomainRigidity.flattened_pair_null line 32