OAI/Analysis/CircleDomains/Topology/SafeGateNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compact forbidden-hit set has a relatively compact neighborhood that avoids both the anchor and the closed target gate. The map is only required to be continuous on the actual domain.

  1. theorem OAI.CircleDomainRigidity.exists_safe_gate_neighborhood line 16