OAI/Analysis/CircleDomains/Sobolev/LocalPairChainRule.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The joint chain rule on the actual open source domain. All temporary global extensions are cut off strictly inside that domain, so no extension across the removed set is assumed.

  1. theorem OAI.CircleDomainRigidity.local_pair_weak_chain line 14