OAI/Probability/SLE/Geometry/PublishedPlanarDiskOpenness.lean

The planar-disk specialization of invariance of domain used for an embedded ribbon coordinate patch. This is an explicit published parameter, not a new axiom. Reference: A. Hatcher, Algebraic Topology (Cambridge, 2002), Theorem 2B.3, p. 172, specialized to n=2 and an open Euclidean disk. https://pi.math.cornell.edu/~hatcher/AT/ATch2.pdf