OAI/Analysis/CircleDomains/Transfer/RetainedRegionAvoidance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact source sets stay outside fixed separated target regions in the actual models.

  1. theorem OAI.CircleDomainRigidity.eventually_image_compact_avoids_closed line 14
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.eventually_avoids_closed line 34
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.eventually_region_over_source_complement line 47