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.
The quotient map is open, and every interval shorter than one embeds in
Statement
Let be the quotient map of The circle as with basepoint . The quotient map is open, and every interval shorter than one embeds in .
More precisely, for every open ,
and is open. If , , and is any of , , , or , then is a homeomorphism, with both sides carrying their subspace topologies.
Facts & Assumptions
Given: The quotient projection , an open set , and an interval of one of the displayed four forms with length .
Let be the quotient projection inducing the quotient topology, with and exactly when (The circle as with basepoint ).
Identify with its canonical copy inside . Then for every real there is exactly one integer with (Integer part: for every real there is exactly one integer with ).
A function is an open map if is open in for every open ; an embedding is a homeomorphism onto its image with the subspace topology (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).
Every constant real-valued function and the identity are continuous, and finite sums and scalar multiples of continuous real-valued 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).
Proof
A real lies in exactly when for some , which by [L1] is equivalent to for some ; hence . Each translate is open: translating by and by gives mutually inverse continuous maps by [L4]. The union is open, so the quotient-topology criterion in [L1] makes open. Thus is open in the sense of [L3], including when .
Suppose and . Then by [L1], while . If , both and satisfy the integer-part inequalities for the real , contrary to uniqueness in [L2]; applying the same argument to excludes . Hence and , so is injective. This also covers a singleton interval; for an empty interval injectivity is vacuous.
The restriction is continuous and is a bijection onto by step 1.2. To prove its inverse continuous, let be relatively open in and . Choose with , and put . Step 1.1 makes open. If and , choose with ; then by [L1] and , so [L2] gives . Thus , and . Every point of therefore has a relative open neighbourhood contained in , so is open in . The empty case has the unique empty inverse. Hence is a homeomorphism onto its image, and therefore an embedding by [L3].
Depends on
The circle as with basepoint
Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological
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
Integer part: for every real there is exactly one integer with