OAI/Analysis/CircleDomains/Selection/GateForbiddenSet.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Hit-location restrictions are avoidance of the union of forbidden parts of the prescribed contours. No closedness is needed for this identity.

  1. def OAI.CircleDomainRigidity.gateForbiddenSet line 14
  2. theorem OAI.CircleDomainRigidity.gateRules_iff_avoids line 16
  3. theorem OAI.CircleDomainRigidity.avoids_gateForbiddenSet_of_avoids_contours line 27