Nuprl Lemma : interval-to-int-bounded
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:{x:ℝ| x ∈ [a, b]} ⟶ ℤ.
∃B:ℕ. ∀x:{x:ℝ| x ∈ [a, b]} . ∃y:{x:ℝ| x ∈ [a, b]} . ((x = y) ∧ (|f y| ≤ B))
Proof
Definitions occuring in Statement :
rccint: [l, u],
i-member: r ∈ I,
rleq: x ≤ y,
req: x = y,
real: ℝ,
absval: |i|,
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
sq_stable: SqStable(P),
implies: P ⇒ Q,
squash: ↓T,
mcompact: mcompact(X;d),
prop: ℙ,
subtype_rel: A ⊆r B,
top: Top,
exists: ∃x:A. B[x],
and: P ∧ Q,
iff: P ⇐⇒ Q,
cand: A c∧ B,
nat: ℕ
Latex:
\mforall{}a:\mBbbR{}. \mforall{}b:\{b:\mBbbR{}| a \mleq{} b\} . \mforall{}f:\{x:\mBbbR{}| x \mmember{} [a, b]\} {}\mrightarrow{} \mBbbZ{}.
\mexists{}B:\mBbbN{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . \mexists{}y:\{x:\mBbbR{}| x \mmember{} [a, b]\} . ((x = y) \mwedge{} (|f y| \mleq{} B))
Date html generated:
2020_05_20-PM-00_01_46
Last ObjectModification:
2019_12_06-PM-01_30_36
Theory : reals
Home
Index