Nuprl Definition : inf
inf(A) = b == lower-bound(A;b) ∧ (∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ (x < (b + e))))))
Definitions occuring in Statement :
lower-bound: lower-bound(A;b),
rset-member: x ∈ A,
rless: x < y,
radd: a + b,
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 :
lower-bound: lower-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,
radd: a + b
FDL editor aliases :
inf
inf
Latex:
inf(A) = b == lower-bound(A;b) \mwedge{} (\mforall{}e:\mBbbR{}. ((r0 < e) {}\mRightarrow{} (\mexists{}x:\mBbbR{}. ((x \mmember{} A) \mwedge{} (x < (b + e))))))
Date html generated:
2016_05_18-AM-08_10_28
Last ObjectModification:
2015_09_23-AM-09_04_24
Theory : reals
Home
Index