OAI/Analysis/CircleDomains/Rigidity/PriorityTracePairs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Priority modification preserves every trace pair whose other coordinate is constant on its cutoff supports.

  1. theorem OAI.CircleDomainRigidity.priorityInfiniteValue_eq_outside_support line 12
  2. theorem OAI.CircleDomainRigidity.priority_trace_pair_null line 22