OAI/Analysis/CircleDomains/Selection/DistinctJunctionBlock.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite block of distinct consecutive 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_through_distinct_dust_junctions line 22