OAI/Analysis/CircleDomains/Rigidity/TraceIntervalPayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Interval payment kills the compressed trace on a null subset of a line. Countable local covers and tail compression then recover the full uncompressed trace, including noninjective compressions.

  1. theorem OAI.CircleDomainRigidity.real_null_image_of_interval_payment line 13
  2. theorem OAI.CircleDomainRigidity.null_image_of_local_null_image line 30
  3. theorem OAI.CircleDomainRigidity.compression_comparison line 46