OAI/Analysis/CircleDomains/Selection/ProtrusionGateGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual protrusion balls give the two target gates and a uniform positive distance from the marked disk. The normalized source map stays outside that disk throughout its physical domain.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.closedGate line 20
  2. def OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.openGate line 21
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.closed_closedGate line 23
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.open_openGate line 26
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.closedGate_subset_openGate line 28
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.closure_openGate line 31
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.infinity_notMem_closure_openGate line 39
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.uniform_gate_gap line 43
  9. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.source_outside_marked_disk line 65