Nuprl Definition : m-interior-point
m-interior-point(X;d;A;p) == ∃M:ℕ+. ∀x:X. ((mdist(d;x;p) ≤ (r1/r(M))) ⇒ (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
FDL editor aliases :
m-interior-point
Latex:
m-interior-point(X;d;A;p) == \mexists{}M:\mBbbN{}\msupplus{}. \mforall{}x:X. ((mdist(d;x;p) \mleq{} (r1/r(M))) {}\mRightarrow{} (x \mmember{} A))
Date html generated:
2020_05_20-AM-11_43_11
Last ObjectModification:
2019_11_07-AM-10_03_41
Theory : reals
Home
Index