OAI/Analysis/CircleDomains/Rigidity/SmoothCommonPointTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The common point trace of every compact smooth target scalar is null on almost every axial line, using only the recorded published inputs.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.smooth_commonPoint_trace_null_of_published_inputs line 23