Nuprl Definition : m-closed-subspace
m-closed-subspace(X;d;A) == ∀x:X. ((∀k:ℕ+. ∃a:A. (mdist(d;x;a) ≤ (r1/r(k)))) ⇒ (x ∈ A))
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,
member: t ∈ T,
natural_number: $n
Definitions occuring in definition :
member: t ∈ T,
int-to-real: r(n),
natural_number: $n,
rdiv: (x/y),
mdist: mdist(d;x;y),
rleq: x ≤ y,
exists: ∃x:A. B[x],
nat_plus: ℕ+,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
m-closed-subspace
Latex:
m-closed-subspace(X;d;A) == \mforall{}x:X. ((\mforall{}k:\mBbbN{}\msupplus{}. \mexists{}a:A. (mdist(d;x;a) \mleq{} (r1/r(k)))) {}\mRightarrow{} (x \mmember{} A))
Date html generated:
2019_10_30-AM-06_31_47
Last ObjectModification:
2019_10_23-PM-06_17_56
Theory : reals
Home
Index