OAI/Analysis/CircleDomains/Topology/RelativelyClosedGates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Collar gates need be closed only on their closed contour. The preimage of a closed target set under a map on the open domain has exactly this property, even when its ambient closure reaches the boundary.

  1. theorem OAI.CircleDomainRigidity.isClosed_contour_gate line 15
  2. theorem OAI.CircleDomainRigidity.gateRule_inter_contour line 31
  3. theorem OAI.CircleDomainRigidity.measurableSet_gateRules_of_inter_closed line 37
  4. theorem OAI.CircleDomainRigidity.codePathLaw_gates_of_inter_closed line 48
  5. theorem OAI.CircleDomainRigidity.IsSubarcLawReduction.code_gates_of_inter_closed line 60
  6. theorem OAI.CircleDomainRigidity.standardBorel_basePathCode_of_inter_closed line 76
  7. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.start_gate_of_inter_closed line 101
  8. theorem OAI.CircleDomainRigidity.CompactRecursiveReduction.physical_start_distance_of_inter_closed line 111