OAI/Analysis/CircleDomains/Selection/MixedCircuitRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed source circuit keeps exactly the same circle values on the actual mixed models and hence supplies a fixed real lift for the Stokes limit.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.MixedModelExhaustion.eventually_circuit_values line 15