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.
FALSE: a function with the intermediate value property on an interval is continuous
Statement
FALSE. If is an interval and has the intermediate value property (The intermediate value property (Darboux property) of a function on an interval: the image of every subinterval is order-convex), then is continuous on (Continuity of at a point of and on : the - condition, its agreement with at a limit point, and continuity at an isolated point).
The converse implication is true and is The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval: every continuous function on an interval has the intermediate value property. The claim above asserts that the implication reverses, and it does not.
Facts & Assumptions
Given: The interval (Intervals of : the nine order-convex forms, nondegeneracy, and length).
For every real there is exactly one integer with , written (Integer part: for every real there is exactly one integer with ); in particular no integer lies strictly between and .
and exist for reals , and a nonempty finite set of reals has a minimum and a maximum (Maximum and minimum of a set, Every nonempty finite set of reals has a maximum and a minimum).
Sums, scalar multiples, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants and the identity; composites 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, A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs).
Intermediate value theorem: a continuous function on takes every value between its values at the endpoints (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and ).
For every real there is a natural with , and the canonical naturals are cofinal in (For every in a complete ordered field there is a natural with , Every complete ordered field is Archimedean, The canonical natural of a field, Canonical naturals are positive and strictly increasing).
, only for , and (Basic properties of the absolute value).
has the intermediate value property on an order-convex exactly when for all in and every between and in either order there is with (The intermediate value property (Darboux property) of a function on an interval: the image of every subinterval is order-convex).
Refutation
Define by , the distance from to the nearest integer, and define by for and .
for every real : writing , the two entries are and , and their minimum is at most their average . Consequently for every .
in the sense that for every integer , with equality for or . Indeed, with : for one has , and for one has .
For every real and every there is with and : take a natural with and put . Then and with , so and .
is continuous on , because for all reals : choose an integer with , which exists by step 2.2; then , and exchanging and gives the other inequality. So witnesses continuity at every point.
For every real and every there is with and : with as in step 2.3 put , so and . If then is an integer and ; if then and , so .
is discontinuous at : , and by step 2.3 every real admits with and , so . Hence no witnesses the continuity condition at for .
is continuous at every with : on the set the map is continuous, and is its composite with ; continuity at a point of that set is continuity of there, since the set contains a whole neighbourhood of inside when .
If then, since , either or . In the first case step 2.3 with gives with and , and ; in the second case step 3.2 with gives with and . Either way .
has the intermediate value property on . Let in and let lie between and in either order; in particular by step 2.1. If then restricted to is continuous by step 4.1, and the intermediate value theorem supplies with .
So is a function on the interval with the intermediate value property that is not continuous on , and the claim in the Statement is false.
Remarks
-
What survives the refutation. The implication continuous intermediate value property is true and is The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval. So is the partial converse for monotone functions: a function satisfying whenever , whose image is order-convex, is continuous (A function on an interval satisfying whenever , whose image is order-convex, is continuous). The witness above is therefore necessarily non-monotone, and it is: it rises and falls infinitely often in every neighbourhood of .
-
The witness fails continuity at exactly one point. That is all a refutation needs, and it is all that is claimed: nothing above says that the failure cannot be worse. Functions with the intermediate value property that are continuous at no point at all do exist, the standard one being Conway's base-13 function; it is not constructed at this point in the reading order, and no statement here depends on it.
-
Nothing above defines the derivative, and Darboux's theorem is not used. The classical source of non-continuous functions with the intermediate value property is the class of derivatives, which have the property by Darboux's theorem; no notion of derivative is available at this point in the reading order, and the witness here is built by hand instead.
Depends on
- The intermediate value property (Darboux property) of a function on an interval: the image of every subinterval is order-convex
- Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$: the $\varepsilon$-$\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point
- Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$
- The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
- Maximum and minimum of a set
- Every nonempty finite set of reals has a maximum and a minimum
- 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
- A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Every complete ordered field is Archimedean
- Basic properties of the absolute value
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Canonical naturals are positive and strictly increasing
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 131 results over 30 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
- Darboux's theorem (analysis) (Wikipedia) (standard reference, not scraped)
- Darboux property (Encyclopedia of Mathematics) (standard reference, not scraped)