OAI/Analysis/CircleDomains/Modulus/LocalizedGeometricPayment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local line payment off a compact source set whose limiting image misses the crossing region.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.line_payment_away_from_compact line 18