Nuprl Lemma : intermediate-value-theorem
∀I:Interval. ∀f:I ⟶ℝ.
(f[x] continuous for x ∈ I
⇒ (∀a,b:{x:ℝ| x ∈ I} .
((f(a) < f(b))
⇒ (∀y:{y:ℝ| y ∈ [f(a), f(b)]} . ∀e:{e:ℝ| r0 < e} . ∃x:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (|f(x) - y| < e)))))
Proof
Definitions occuring in Statement :
continuous: f[x] continuous for x ∈ I,
r-ap: f(x),
rfun: I ⟶ℝ,
rccint: [l, u],
i-member: r ∈ I,
interval: Interval,
rless: x < y,
rabs: |x|,
rmin: rmin(x;y),
rmax: rmax(x;y),
rsub: x - y,
int-to-real: r(n),
real: ℝ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
rneq: x ≠ y,
or: P ∨ Q,
so_apply: x[s],
r-ap: f(x),
uall: ∀[x:A]. B[x],
rfun: I ⟶ℝ,
prop: ℙ,
uimplies: b supposing a,
sq_stable: SqStable(P),
squash: ↓T,
so_lambda: λ2x.t[x],
label: ...$L... t,
iff: P ⇐⇒ Q,
and: P ∧ Q,
guard: {T},
rev_implies: P ⇐ Q,
cand: A c∧ B,
subtype_rel: A ⊆r B,
subinterval: I ⊆ J ,
rev_uimplies: rev_uimplies(P;Q),
rge: x ≥ y,
rgt: x > y,
not: ¬A,
exists: ∃x:A. B[x],
continuous: f[x] continuous for x ∈ I,
icompact: icompact(I),
i-nonvoid: i-nonvoid(I),
sq_exists: ∃x:A [B[x]],
false: False,
l_all: (∀x∈L.P[x]),
int_seg: {i..j-},
nat: ℕ,
lelt: i ≤ j < k,
rless: x < y,
real: ℝ,
nat_plus: ℕ+,
ge: i ≥ j ,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
rleq: x ≤ y,
rnonneg: rnonneg(x),
le: A ≤ B,
full-partition: full-partition(I;p),
select: L[n],
cons: [a / b],
i-member: r ∈ I,
rccint: [l, u],
partition: partition(I),
less_than: a < b,
rbetween: x≤y≤z,
uiff: uiff(P;Q),
req_int_terms: t1 ≡ t2,
inf: inf(A) = b,
lower-bound: lower-bound(A;b),
rrange: f[x](x∈I),
rset-member: x ∈ A,
true: True,
rdiv: (x/y),
i-finite: i-finite(I),
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
bool: 𝔹,
unit: Unit,
it: ⋅,
bfalse: ff,
sq_type: SQType(T),
bnot: ¬bb,
nil: [],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
absval: |i|
Latex:
\mforall{}I:Interval. \mforall{}f:I {}\mrightarrow{}\mBbbR{}.
(f[x] continuous for x \mmember{} I
{}\mRightarrow{} (\mforall{}a,b:\{x:\mBbbR{}| x \mmember{} I\} .
((f(a) < f(b))
{}\mRightarrow{} (\mforall{}y:\{y:\mBbbR{}| y \mmember{} [f(a), f(b)]\} . \mforall{}e:\{e:\mBbbR{}| r0 < e\} .
\mexists{}x:\{x:\mBbbR{}| x \mmember{} [rmin(a;b), rmax(a;b)]\} . (|f(x) - y| < e)))))
Date html generated:
2020_05_20-PM-00_27_48
Last ObjectModification:
2020_01_06-PM-01_59_16
Theory : reals
Home
Index