How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
is a homeomorphism from to the unit circle
Statement
Let
with the Euclidean subspace topology. The function
is a homeomorphism. Thus is a homeomorphism from to the unit circle and sends to .
Facts & Assumptions
Given: The quotient projection and the unit circle .
If is a quotient map and a continuous function is constant on every fibre of , then there is exactly one continuous function with (For a quotient map , a map out of is continuous iff its composite with is; a continuous map on constant on the fibres of factors uniquely through ; and a composite of quotient maps is a quotient map).
The functions and are differentiable on , with and (The derivatives of sine and cosine are cosine and minus sine).
A real function differentiable on a set is continuous at every point of that set (A function differentiable at is continuous at ).
If , is a metric space, , and , then is continuous exactly when all its coordinate functions are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).
Both sine and cosine have period , and no smaller positive number is a common period (The zero sets of sine and cosine and the least positive common period 2 pi).
The map is a bijection from onto ( is a bijection from onto the real unit circle).
is compact and path-connected ( is compact and path-connected).
A continuous bijection from a compact space to a Hausdorff space is a homeomorphism (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).
Every metric space is Hausdorff (Distinct points of a metric space have disjoint balls around them).
Every constant real-valued function and the identity are continuous, and finite sums, products, and scalar multiples of continuous functions are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).
The quotient projection induces the quotient topology and satisfies exactly when (The circle as with basepoint ).
For every real there is exactly one integer with (Integer part: for every real there is exactly one integer with ).
The Euclidean distance is a metric on ( as the set of functions , and , , are metrics on it).
A subspace of a metrizable space is metrizable by the restricted metric (Every subspace of a metrizable space is metrizable and every subspace of a first countable space is first countable, the metric case being the subspace metric already identified with the subspace topology).
A map into a subspace is continuous if and only if its composite with the inclusion into the ambient space is continuous (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).
and is the smallest positive zero of cosine (Pi as twice the smallest positive zero of cosine).
A composite of continuous maps is continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).
Proof
Define . By [L2] and [L3], sine and cosine are continuous; by [L10], is continuous; hence their composites are continuous by [L17], and [L4] makes continuous. For with and from [L12], periodicity [L5] gives , while [L6] applied to , using [L16], shows ; [L15] therefore makes continuous. Finally [L5] gives for every integer .
By [L11], the fibres of are precisely the integer-translation classes, so step 1.1 says that is constant on every fibre. The quotient universal property [L1] gives a unique continuous satisfying , namely .
To prove surjectivity, let . By [L6], for a unique ; since [L16] gives , the real lies in and . For injectivity, suppose . Write and with and using [L12]. Periodicity [L5] gives , and the injectivity in [L6] on gives , hence . Thus , so [L11] gives . Therefore is bijective.
The source is compact by [L7]. By [L13], is metrizable; by [L14], its subspace is metrizable, and [L9] makes Hausdorff. Thus the continuous bijection from steps 2.1 and 3.1 is a homeomorphism by [L8]. Finally [L2] gives .
Depends on
- The circle as $S^1=\mathbb R/\mathbb Z$ with basepoint $[0]$
- $\mathbb R/\mathbb Z$ is compact and path-connected
- For a quotient map $q : X \to Y$, a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$; and a composite of quotient maps is a quotient map
- The derivatives of sine and cosine are cosine and minus sine
- A function differentiable at $c$ is continuous at $c$
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
- Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous
- A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
- Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
- The zero sets of sine and cosine and the least positive common period 2 pi
- $t\mapsto(\cos t,\sin t)$ is a bijection from $[0,2\pi)$ onto the real unit circle
- Pi as twice the smallest positive zero of cosine
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
- A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism
- $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it
- Every subspace of a metrizable space is metrizable and every subspace of a first countable space is first countable, the metric case being the subspace metric already identified with the subspace topology
- Distinct points of a metric space have disjoint balls around them
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 239 results over 39 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Jonathan Wise, Math 6210 Lecture Notes, Week 3, Section 3.4, Proposition 3.4 (standard reference, not scraped)
- NIST Digital Library of Mathematical Functions, Chapter 4 (standard reference, not scraped)