OAI/Analysis/CircleDomains/Topology/CompactCoreRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every fixed compact core is eventually retained

The plane domains exhaust the source, and every finite model contains a fixed neighborhood of infinity. These two facts give eventual retention of any compact sphere core; no extra exhaustion hypothesis is required.

  1. theorem OAI.CircleDomainRigidity.eventually_compact_subset_model line 18