OAI/Analysis/CircleDomains/Transfer/SourceStokesEventual.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Discard the finite initial segment before a source circuit has been retained. The limit exclusion requires only eventual model identities.

  1. theorem OAI.CircleDomainRigidity.boundaryExclusionSet_excludes_eventual_source_stokes line 13