OAI/Analysis/CircleDomains/Transfer/PrincipalSubordinateMixedTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the common mixed model from subordinate graph geometry, using the original global real branches at every real coordinate.

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