OAI/Analysis/CircleDomains/Rigidity/ModelSourceTracePairs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The null trace pairs on the actual target complement pull back to all source ends through the constructed surjective projection.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.section_target_complement line 16
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.source_height_trace_pairs line 40
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.source_height_horizontal_pair line 70