OAI/Analysis/CircleDomains/Transfer/PrincipalAbsentMixedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exterior replacements preserve every full-mask real coordinate, including its exact real collar branch and its transported real filling.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.principal_absent_mixed_transfer line 15