Nuprl Definition : rat-point-in-cube
rat-point-in-cube(k;x;c) == ∀i:ℕk. (((fst((c i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c i)))))
Definitions occuring in Statement :
qle: r ≤ s,
int_seg: {i..j-},
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
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,
and: P ∧ Q,
pi1: fst(t),
qle: r ≤ s,
pi2: snd(t),
apply: f a
FDL editor aliases :
rat-point-in-cube
Latex:
rat-point-in-cube(k;x;c) == \mforall{}i:\mBbbN{}k. (((fst((c i))) \mleq{} (x i)) \mwedge{} ((x i) \mleq{} (snd((c i)))))
Date html generated:
2020_05_20-AM-09_18_00
Last ObjectModification:
2019_11_02-PM-04_18_14
Theory : rationals
Home
Index