OAI/Analysis/CircleDomains/Topology/TerminalBoundaryLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Inverse images approach the assigned terminal boundary

A target sequence approaching an assigned complementary component has preimages eventually in every neighborhood of the corresponding physical terminal boundary. Compactness and the proved component assignment replace any assumption of a boundary extension of the uniformizing map.

  1. instance OAI.CircleDomainRigidity.sphereFirstCountableTopology line 21
  2. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.source_cluster_mem_boundary line 24
  3. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.inverse_eventually_near_boundary line 62
  4. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.inverse_tendsto_boundary line 85