OAI/Analysis/CircleDomains/Selection/AnchoredDustBlock.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite block of possibly repeated limiting dust junctions can be replaced by one allowed true path. The original true-piece limits and one paid toll per junction cover the replacement, up to any positive error.

  1. theorem OAI.CircleDomainRigidity.exists_path_replacing_anchored_dust_block line 23