OAI/Analysis/CircleDomains/Topology/SimpleSubarcRelation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual Borel relation used to select simple subarcs, including the endpoint equalities and containment in the original path image.

  1. def OAI.CircleDomainRigidity.simpleSubarcRelation line 16
  2. theorem OAI.CircleDomainRigidity.measurableSet_simpleSubarcRelation line 22
  3. theorem OAI.CircleDomainRigidity.measurableSet_simpleTerminalArcRelation line 33