OAI/Analysis/CircleDomains/Selection/OrderedHoleIntegration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts for a bounded filling of actual ordered closed intervals. Finite variation constructs every endpoint trace used below.

  1. theorem OAI.CircleDomainRigidity.filled_integration_of_ordered_holes line 12