Nuprl Definition : rat-point-in-cube-interior
rat-point-in-cube-interior(k;x;a) ==
∀i:ℕk
((((fst((a i))) ≤ (x i)) ∧ ((x i) ≤ (snd((a i)))))
∧ (fst((a i)) < snd((a i)) ⇒ (fst((a i)) < x i ∧ x i < snd((a i)))))
Definitions occuring in Statement :
qle: r ≤ s,
qless: r < s,
int_seg: {i..j-},
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
qle: r ≤ s,
implies: P ⇒ Q,
and: P ∧ Q,
pi1: fst(t),
qless: r < s,
pi2: snd(t),
apply: f a
FDL editor aliases :
rat-point-in-cube-interior
Latex:
rat-point-in-cube-interior(k;x;a) ==
\mforall{}i:\mBbbN{}k
((((fst((a i))) \mleq{} (x i)) \mwedge{} ((x i) \mleq{} (snd((a i)))))
\mwedge{} (fst((a i)) < snd((a i)) {}\mRightarrow{} (fst((a i)) < x i \mwedge{} x i < snd((a i)))))
Date html generated:
2020_05_20-AM-09_18_43
Last ObjectModification:
2019_11_02-PM-07_04_37
Theory : rationals
Home
Index