OAI/Analysis/CircleDomains/Selection/UngatedCodes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A contour already contained in its allowed gate imposes no restriction. This includes the ungated endpoint problems used in the transfinite recursion.

  1. theorem OAI.CircleDomainRigidity.measurableSet_endpointCode_of_vacuous_gates line 19
  2. theorem OAI.CircleDomainRigidity.standardBorel_basePathCode_of_vacuous_gates line 41