Nuprl Definition : m-open
m-open(X;d;x.A[x]) == ∀x:X. (A[x] ⇒ (∃k:ℕ+. ∀y:X. ((mdist(d;x;y) ≤ (r1/r(k))) ⇒ A[y])))
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rdiv: (x/y),
rleq: x ≤ y,
int-to-real: r(n),
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
FDL editor aliases :
m-open
Latex:
m-open(X;d;x.A[x]) == \mforall{}x:X. (A[x] {}\mRightarrow{} (\mexists{}k:\mBbbN{}\msupplus{}. \mforall{}y:X. ((mdist(d;x;y) \mleq{} (r1/r(k))) {}\mRightarrow{} A[y])))
Date html generated:
2020_05_20-AM-11_53_58
Last ObjectModification:
2020_01_12-PM-00_34_05
Theory : reals
Home
Index