OAI/Analysis/CircleDomains/Topology/FiniteJumpCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common compactness for finitely many shrinking new jumps and true pieces, retaining fixed old-jump costs in the limiting total budget.

  1. theorem OAI.CircleDomainRigidity.exists_joint_finite_jump_limits line 17