OAI/Analysis/CircleDomains/Topology/ComponentSphereRealization.lean

The sphere realization of the actual component quotient. The map is constructed as a uniform limit of shrinking homeomorphisms. A simultaneous quotient-valued inverse limit proves the exact, rather than approximate, fiber identity. No sphere decomposition theorem is assumed.