nLab Jordan curve theorem

Redirected from "Jordan--Brouwer separation theorem".
Contents

Context

Topology

topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory

Introduction

Basic concepts

Universal constructions

Extra stuff, structure, properties

Examples

Basic statements

Theorems

Analysis Theorems

topological homotopy theory

Contents

Idea

The Jordan curve theorem is a basic fact in topology. It stands out as having a statement that intuitively seems completely obvious, but which turns out to require a non-trivial formal proof.

The theorem states that every continuous loop (where a loop is a closed curve) in the Euclidean plane which does not intersect itself (a Jordan curve) divides the plane into two disjoint subsets (the connected components of the curve's complement), a bounded region inside the curve, and an unbounded region outside of it, each of which has the original curve as its boundary.

In constructive mathematics

Given a notion of real number \mathbb{R} in constructive mathematics, a Jordan curve consists of a set JJ with a specific injection i:J 2i:J \to \mathbb{R}^2 into the Euclidean plane 2\mathbb{R}^2, and a homeomorphism h:𝕊 1im(i)h:\mathbb{S}^1 \to \mathrm{im}(i) from the topological unit circle 𝕊 1\mathbb{S}^1 to the image of the subset injection.

section under construction

In constructive mathematics, the Jordan curve theorem is stated as

Theorem

Given a Jordan curve JJ, two points aa and bb can be constructed off of JJ, such that given any point cc off of JJ, we can construct a polygonal path that is bounded away from JJ, and that joins cc to one of aa or bb, and any polygonal path joining aa and bb comes arbitrarily close to JJ.

In cohesive homotopy type theory

In cohesive homotopy type theory, the Jordan curve theorem says that:

Let JJ be a Jordan curve in the Euclidean plane J 2J \subseteq \mathbb{R}^2 with injection i:J 2i:J \hookrightarrow \mathbb{R}^2, and let 2J\mathbb{R}^2 \setminus J be the set of all points in 2\mathbb{R}^2 which is away from all points in the Jordan curve JJ.

2J x:R 2 a:J|xi(a)|>0\mathbb{R}^2 \setminus J \coloneqq \sum_{x:R^2} \prod_{a:J} \vert x - i(a) \vert \gt 0

The shape of 2J\mathbb{R}^2 \setminus J is equivalent to 𝟙+S 1\mathbb{1} + S^1, where 𝟙\mathbb{1} is the unit type and S 1S^1 is the circle type.

ʃ( 2J)𝟙+S 1\esh(\mathbb{R}^2 \setminus J) \simeq \mathbb{1} + S^1

Generalization

The Jordan–Brouwer separation theorem states that, in the Cartesian space n\mathbb{R}^n, every simple closed continuous hypersurface (defined as the image of a continuous injection from the sphere S n1S^{n-1}) has an exterior with two connected components, one bounded (the inside of the hypersurface) and one unbounded, each of which has the original hypersurface as its boundary. (Furthermore, the continuous map defining the hypersurface can be extended to an auto-homeomorphism of n\mathbb{R}^n under which the inside and outside appear as the images of the inside and outside of the sphere.)

References

Last revised on June 26, 2024 at 02:05:26. See the history of this page for a list of all contributions to it.