Nuprl Definition : weighted-mean-properties
weighted-mean-properties(I;F) ==
(∀x:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} . ((F x x r s) = x))
∧ (∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r,s:{s:ℝ| r0 < s} .
((a = (F a b r1 r0)) ∧ ((F a b r1 r0) < (F a b r s)) ∧ ((F a b r s) < (F a b r0 r1)) ∧ ((F a b r0 r1) = b)))
∧ (∀a,b:{b:ℝ| b ∈ I} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| (r0 < s) ∧ (r0 < (r + s))} . ∀t:{t:ℝ| r0 < t} .
((F a b (r * t) (s * t)) = (F a b r s)))
∧ (∀x,y:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} . ∀X,Y:{x:ℝ| x ∈ I} . ∀R:{R:ℝ|
(r0 ≤ R)
∧ (r0 < (r + R))} \000C.
∀S:{S:ℝ| ((r0 ≤ S) ∧ (r0 < (s + S))) ∧ (r0 < (R + S))} .
((F (F x y r s) (F X Y R S) (r + s) (R + S)) = (F (F x X r R) (F y Y s S) (r + R) (s + S))))
∧ (∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| r0 ≤ s} . ∀t:{t:ℝ| s < t} .
((F a b r s) < (F a b r t)))
∧ (∀x,y:{x:ℝ| x ∈ I} . ∀z:{z:ℝ| (z ∈ I) ∧ (y < z)} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| r0 < s} . ((F x y r s) < (F x z r s)\000C))
Definitions occuring in Statement :
i-member: r ∈ I,
rleq: x ≤ y,
rless: x < y,
req: x = y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
natural_number: $n
Definitions occuring in definition :
real: ℝ,
set: {x:A| B[x]} ,
all: ∀x:A. B[x],
and: P ∧ Q,
natural_number: $n,
int-to-real: r(n),
apply: f a,
req: x = y,
rless: x < y,
i-member: r ∈ I,
radd: a + b,
rleq: x ≤ y,
rmul: a * b
FDL editor aliases :
weighted-mean-properties
Latex:
weighted-mean-properties(I;F) ==
(\mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . \mforall{}r:\{r:\mBbbR{}| r0 \mleq{} r\} . \mforall{}s:\{s:\mBbbR{}| (r0 \mleq{} s) \mwedge{} (r0 < (r + s))\} . ((F x x r s) = x))
\mwedge{} (\mforall{}a:\{a:\mBbbR{}| a \mmember{} I\} . \mforall{}b:\{b:\mBbbR{}| (b \mmember{} I) \mwedge{} (a < b)\} . \mforall{}r,s:\{s:\mBbbR{}| r0 < s\} .
((a = (F a b r1 r0))
\mwedge{} ((F a b r1 r0) < (F a b r s))
\mwedge{} ((F a b r s) < (F a b r0 r1))
\mwedge{} ((F a b r0 r1) = b)))
\mwedge{} (\mforall{}a,b:\{b:\mBbbR{}| b \mmember{} I\} . \mforall{}r:\{r:\mBbbR{}| r0 < r\} . \mforall{}s:\{s:\mBbbR{}| (r0 < s) \mwedge{} (r0 < (r + s))\} . \mforall{}t:\{t:\mBbbR{}| r0 < t\} .
((F a b (r * t) (s * t)) = (F a b r s)))
\mwedge{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . \mforall{}r:\{r:\mBbbR{}| r0 \mleq{} r\} . \mforall{}s:\{s:\mBbbR{}| (r0 \mleq{} s) \mwedge{} (r0 < (r + s))\} . \mforall{}X,Y:\{x:\mBbbR{}| x \mmember{} I\} \000C.
\mforall{}R:\{R:\mBbbR{}| (r0 \mleq{} R) \mwedge{} (r0 < (r + R))\} . \mforall{}S:\{S:\mBbbR{}| ((r0 \mleq{} S) \mwedge{} (r0 < (s + S))) \mwedge{} (r0 < (R + S))\} .
((F (F x y r s) (F X Y R S) (r + s) (R + S)) = (F (F x X r R) (F y Y s S) (r + R) (s + S))))
\mwedge{} (\mforall{}a:\{a:\mBbbR{}| a \mmember{} I\} . \mforall{}b:\{b:\mBbbR{}| (b \mmember{} I) \mwedge{} (a < b)\} . \mforall{}r:\{r:\mBbbR{}| r0 < r\} . \mforall{}s:\{s:\mBbbR{}| r0 \mleq{} s\} . \mforall{}t:\{t:\mBbbR{}|
s < t\} .
((F a b r s) < (F a b r t)))
\mwedge{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . \mforall{}z:\{z:\mBbbR{}| (z \mmember{} I) \mwedge{} (y < z)\} . \mforall{}r:\{r:\mBbbR{}| r0 \mleq{} r\} . \mforall{}s:\{s:\mBbbR{}| r0 < s\} .
((F x y r s) < (F x z r s)))
Date html generated:
2017_10_04-PM-11_10_19
Last ObjectModification:
2017_07_29-PM-09_31_24
Theory : reals_2
Home
Index