Nuprl Definition : sup
sup(A) = b == A ≤ b ∧ (∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ ((b - e) < x)))))
Definitions occuring in Statement :
upper-bound: A ≤ b,
rset-member: x ∈ A,
rless: x < y,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
natural_number: $n
Definitions occuring in definition :
upper-bound: A ≤ b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
int-to-real: r(n),
natural_number: $n,
exists: ∃x:A. B[x],
real: ℝ,
and: P ∧ Q,
rset-member: x ∈ A,
rless: x < y,
rsub: x - y
FDL editor aliases :
sup
sup
Latex:
sup(A) = b == A \mleq{} b \mwedge{} (\mforall{}e:\mBbbR{}. ((r0 < e) {}\mRightarrow{} (\mexists{}x:\mBbbR{}. ((x \mmember{} A) \mwedge{} ((b - e) < x)))))
Date html generated:
2016_05_18-AM-08_10_00
Last ObjectModification:
2015_09_23-AM-09_04_19
Theory : reals
Home
Index