OAI/Analysis/CircleDomains/Topology/CompactExitPenalty.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact separation supplies the positive physical width and hence an actual bounded indicator penalty. No path-cost lower bound is assumed.

  1. theorem OAI.CircleDomainRigidity.exists_compact_exit_penalty line 20