OAI/Analysis/CircleDomains/Topology/SphereCoreExhaustion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual source cores for domains containing infinity

The open connected cores exhaust the given domain. Their finite closures, with infinity added, are compact subsets of the domain and can therefore be prescribed in the finite-transfer construction.

  1. theorem OAI.CircleDomainRigidity.isClosed_finite_set_with_infty line 21
  2. theorem OAI.CircleDomainRigidity.exists_sphere_connected_core_exhaustion line 33