ClosedSetPathLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform limits of successively improved ambient paths lie in the closed target set, retaining the endpoints and all summable error bounds.