OAI/Analysis/CircleDomains/Rigidity/MatchedIntervalCoverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual matched end relation covers all scalar values between selected endpoints of a source segment. No continuity of the selection at a nontrivial complementary component is assumed.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.targetFiber_isPreconnected line 17
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.interval_fiber_scalar_coverage line 32
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.interval_scalar_coverage line 59