OAI/Analysis/CircleDomains/Rigidity/AxialSlicesFromTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The compact scalar used in the slice proof is constructed from the actual relation. One typical line supports every segment and finite family of removed source disks inside the working disk.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.axial_slices_of_trace line 18