OAI/Analysis/CircleDomains/Selection/AssignedStokes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Stokes for selected holes of an actual finite model. The real collar branches and their bounds are transported from the corresponding source terminal boundaries. Holes outside the chosen Jordan mask need no branch.

  1. theorem OAI.CircleDomainRigidity.assigned_model_stokes_bound line 17