Nuprl Definition : trans-kernel-fun
trans-kernel-fun(rv;e;f) ==
(∀h1,h2:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2)))
∧ (∀h:{h:Point| h ⋅ e = r0} . ((f h r0) = r0))
∧ (∀h:{h:Point| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2))))
∧ (∀h:{h:Point| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r))
Definitions occuring in Statement :
rv-ip: x ⋅ y,
rneq: x ≠ y,
rless: x < y,
req: x = y,
int-to-real: r(n),
real: ℝ,
ss-sep: x # y,
ss-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
natural_number: $n
Definitions occuring in definition :
or: P ∨ Q,
ss-sep: x # y,
rneq: x ≠ y,
and: P ∧ Q,
implies: P ⇒ Q,
rless: x < y,
set: {x:A| B[x]} ,
ss-point: Point,
rv-ip: x ⋅ y,
int-to-real: r(n),
natural_number: $n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
real: ℝ,
req: x = y,
apply: f a
FDL editor aliases :
trans-kernel-fun
Latex:
trans-kernel-fun(rv;e;f) ==
(\mforall{}h1,h2:\{h:Point| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. (f h1 t1 \mneq{} f h2 t2 {}\mRightarrow{} (h1 \# h2 \mvee{} t1 \mneq{} t2)))
\mwedge{} (\mforall{}h:\{h:Point| h \mcdot{} e = r0\} . ((f h r0) = r0))
\mwedge{} (\mforall{}h:\{h:Point| h \mcdot{} e = r0\} . \mforall{}t1,t2:\mBbbR{}. ((t1 < t2) {}\mRightarrow{} ((f h t1) < (f h t2))))
\mwedge{} (\mforall{}h:\{h:Point| h \mcdot{} e = r0\} . \mforall{}r:\mBbbR{}. \mexists{}t:\mBbbR{}. ((f h t) = r))
Date html generated:
2017_10_05-AM-00_22_50
Last ObjectModification:
2017_06_26-PM-10_02_36
Theory : inner!product!spaces
Home
Index