OAI/Analysis/CircleDomains/Topology/ConnectedCoreNeighborhood.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact connected neighborhoods inside the source

A compact subset of a domain containing infinity lies strictly inside a compact connected subset of that domain which also contains a neighborhood of infinity. This lets successive finite Jordan cores retain earlier ones.

  1. theorem OAI.CircleDomainRigidity.closure_finite_domain_with_infty line 20
  2. theorem OAI.CircleDomainRigidity.isConnected_finite_domain_with_infty line 31
  3. theorem OAI.CircleDomainRigidity.exists_compact_connected_core_neighborhood line 48