OAI/Analysis/CircleDomains/Selection/ApproximateFiniteConcatenation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Approximate pieces can be concatenated across singleton anchors, with one prescribed budget at each internal junction and one total error.

  1. theorem OAI.CircleDomainRigidity.exists_allowed_approximate_finite_concatenation line 19