:: RLAFFIN2 semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V66() non empty-membered V273() V274() V276() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() non empty-membered V271() V273() Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of NAT
K495(1) is ext-real set
COMPLEX is non empty non trivial non finite complex-membered V66() non empty-membered set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V66() non empty-membered set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V66() non empty-membered set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V50() non empty-membered set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite non empty-membered set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V50() non empty-membered set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite non empty-membered set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:REAL,REAL:] is non empty non trivial non finite non empty-membered set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite non empty-membered set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:RAT,RAT:] is non empty non trivial non finite non empty-membered set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite non empty-membered set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:INT,INT:] is non empty non trivial non finite non empty-membered set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite non empty-membered set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() V53() non empty-membered set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() V53() non empty-membered set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite non empty-membered set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() non empty-membered V271() V273() set
bool omega is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
{} is Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() set
the Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() set is Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() set
2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of NAT
[:NAT,REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set
K541() is set
{{}} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() set
{{}} * is functional FinSequence-membered FinSequenceSet of {{}}
[:({{}} *),{{}}:] is Relation-like RAT -valued INT -valued V50() V51() V52() V53() set
bool [:({{}} *),{{}}:] is non empty set
PFuncs (({{}} *),{{}}) is set
0 is Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() V31() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() Element of NAT
Seg 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
{1} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered with_non-empty_elements non empty-membered V271() V272() V273() V274() V275() set
Seg 2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
{1,2} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered with_non-empty_elements non empty-membered V271() V272() V273() V274() V275() set
union {} is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
V is V21() real ext-real Element of REAL
1 - V is V21() real ext-real Element of REAL
1 / (1 - V) is V21() real ext-real Element of REAL
1 - (1 / (1 - V)) is V21() real ext-real Element of REAL
B is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of B is non empty set
S is Element of the carrier of B
V * S is Element of the carrier of B
(1 - (1 / (1 - V))) * S is Element of the carrier of B
BS is Element of the carrier of B
(1 - V) * BS is Element of the carrier of B
(V * S) + ((1 - V) * BS) is Element of the carrier of B
U is Element of the carrier of B
(1 / (1 - V)) * U is Element of the carrier of B
((1 / (1 - V)) * U) + ((1 - (1 / (1 - V))) * S) is Element of the carrier of B
U - (V * S) is Element of the carrier of B
1 - 1 is V21() real ext-real Element of REAL
(1 / (1 - V)) * (1 - V) is V21() real ext-real Element of REAL
(1 / (1 - V)) * (V * S) is Element of the carrier of B
(1 / (1 - V)) * V is V21() real ext-real Element of REAL
((1 / (1 - V)) * V) * S is Element of the carrier of B
1 - (1 - V) is V21() real ext-real Element of REAL
(1 - (1 - V)) / (1 - V) is V21() real ext-real Element of REAL
((1 - (1 - V)) / (1 - V)) * S is Element of the carrier of B
(1 - V) / (1 - V) is V21() real ext-real Element of REAL
(1 / (1 - V)) - ((1 - V) / (1 - V)) is V21() real ext-real Element of REAL
((1 / (1 - V)) - ((1 - V) / (1 - V))) * S is Element of the carrier of B
(1 / (1 - V)) - 1 is V21() real ext-real Element of REAL
((1 / (1 - V)) - 1) * S is Element of the carrier of B
1 * BS is Element of the carrier of B
(1 / (1 - V)) * ((1 - V) * BS) is Element of the carrier of B
((1 / (1 - V)) * U) - ((1 / (1 - V)) * (V * S)) is Element of the carrier of B
- (((1 / (1 - V)) - 1) * S) is Element of the carrier of B
((1 / (1 - V)) * U) + (- (((1 / (1 - V)) - 1) * S)) is Element of the carrier of B
- S is Element of the carrier of B
((1 / (1 - V)) - 1) * (- S) is Element of the carrier of B
((1 / (1 - V)) * U) + (((1 / (1 - V)) - 1) * (- S)) is Element of the carrier of B
- ((1 / (1 - V)) - 1) is V21() real ext-real Element of REAL
(- ((1 / (1 - V)) - 1)) * S is Element of the carrier of B
((1 / (1 - V)) * U) + ((- ((1 / (1 - V)) - 1)) * S) is Element of the carrier of B
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of the carrier of V
{B} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
S is Element of bool the carrier of V
S \ {B} is Element of bool the carrier of V
conv (S \ {B}) is convex Element of bool the carrier of V
BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
Sum BS is Element of the carrier of V
BS . B is V21() real ext-real Element of REAL
(BS . B) * B is Element of the carrier of V
1 - (BS . B) is V21() real ext-real Element of REAL
1 / (BS . B) is V21() real ext-real Element of REAL
(1 / (BS . B)) * (Sum BS) is Element of the carrier of V
1 - (1 / (BS . B)) is V21() real ext-real Element of REAL
Carrier BS is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not BS . b₁ = 0 } is set
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of {B}
X . B is V21() real ext-real Element of REAL
1 * B is Element of the carrier of V
1 - 1 is V21() real ext-real Element of REAL
y is non empty Element of bool the carrier of V
BS - X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- 1 is non empty V21() real ext-real non positive negative Element of REAL
(- 1) * X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
BS + (- X) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 / (1 - (BS . B)) is V21() real ext-real Element of REAL
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
(1 / (1 - (BS . B))) * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
Carrier ((1 / (1 - (BS . B))) * U) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not ((1 / (1 - (BS . B))) * U) . b₁ = 0 } is set
U . B is V21() real ext-real Element of REAL
(BS . B) - (BS . B) is V21() real ext-real Element of REAL
((1 / (1 - (BS . B))) * U) . B is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * ((BS . B) - (BS . B)) is V21() real ext-real Element of REAL
Carrier X is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0 } is set
xBS is Element of the carrier of V
((1 / (1 - (BS . B))) * U) . xBS is V21() real ext-real Element of REAL
U . xBS is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * (U . xBS) is V21() real ext-real Element of REAL
BS . xBS is V21() real ext-real Element of REAL
X . xBS is V21() real ext-real Element of REAL
(BS . xBS) - (X . xBS) is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * ((BS . xBS) - (X . xBS)) is V21() real ext-real Element of REAL
sum U is V21() real ext-real Element of REAL
sum BS is V21() real ext-real Element of REAL
sum X is V21() real ext-real Element of REAL
(sum BS) - (sum X) is V21() real ext-real Element of REAL
(sum BS) - (BS . B) is V21() real ext-real Element of REAL
sum ((1 / (1 - (BS . B))) * U) is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * (1 - (BS . B)) is V21() real ext-real Element of REAL
xBS is non empty Element of bool the carrier of V
BU is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of xBS
Sum BU is Element of the carrier of V
xU is Element of the carrier of V
(1 - (BS . B)) * xU is Element of the carrier of V
((BS . B) * B) + ((1 - (BS . B)) * xU) is Element of the carrier of V
(1 - (1 / (BS . B))) * xU is Element of the carrier of V
((1 / (BS . B)) * (Sum BS)) + ((1 - (1 / (BS . B))) * xU) is Element of the carrier of V
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of xBS : b₁ in ConvexComb V } is set
Sum U is Element of the carrier of V
Sum X is Element of the carrier of V
(Sum BS) - (Sum X) is Element of the carrier of V
(Sum BS) - ((BS . B) * B) is Element of the carrier of V
(1 / (1 - (BS . B))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
(1 - (BS . B)) * ((1 / (1 - (BS . B))) * ((Sum BS) - ((BS . B) * B))) is Element of the carrier of V
(1 - (BS . B)) * (1 / (1 - (BS . B))) is V21() real ext-real Element of REAL
((1 - (BS . B)) * (1 / (1 - (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
1 * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
(BS . B) / (BS . B) is V21() real ext-real Element of REAL
((BS . B) / (BS . B)) - (1 / (BS . B)) is V21() real ext-real Element of REAL
(BS . B) - 1 is V21() real ext-real Element of REAL
((BS . B) - 1) / (BS . B) is V21() real ext-real Element of REAL
- (1 - (BS . B)) is V21() real ext-real Element of REAL
(- (1 - (BS . B))) / (BS . B) is V21() real ext-real Element of REAL
(1 - (BS . B)) / (BS . B) is V21() real ext-real Element of REAL
- ((1 - (BS . B)) / (BS . B)) is V21() real ext-real Element of REAL
(1 - (1 / (BS . B))) * (Sum BU) is Element of the carrier of V
(- ((1 - (BS . B)) / (BS . B))) * ((1 / (1 - (BS . B))) * ((Sum BS) - ((BS . B) * B))) is Element of the carrier of V
(- ((1 - (BS . B)) / (BS . B))) * (1 / (1 - (BS . B))) is V21() real ext-real Element of REAL
((- ((1 - (BS . B)) / (BS . B))) * (1 / (1 - (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
((1 - (BS . B)) / (BS . B)) * (1 / (1 - (BS . B))) is V21() real ext-real Element of REAL
- (((1 - (BS . B)) / (BS . B)) * (1 / (1 - (BS . B)))) is V21() real ext-real Element of REAL
(- (((1 - (BS . B)) / (BS . B)) * (1 / (1 - (BS . B))))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
(1 - (BS . B)) / (1 - (BS . B)) is V21() real ext-real Element of REAL
((1 - (BS . B)) / (1 - (BS . B))) * (1 / (BS . B)) is V21() real ext-real Element of REAL
- (((1 - (BS . B)) / (1 - (BS . B))) * (1 / (BS . B))) is V21() real ext-real Element of REAL
(- (((1 - (BS . B)) / (1 - (BS . B))) * (1 / (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
1 * (1 / (BS . B)) is V21() real ext-real Element of REAL
- (1 * (1 / (BS . B))) is V21() real ext-real Element of REAL
(- (1 * (1 / (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
- (1 / (BS . B)) is V21() real ext-real Element of REAL
(- (1 / (BS . B))) * (Sum BS) is Element of the carrier of V
(- (1 / (BS . B))) * ((BS . B) * B) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) - ((- (1 / (BS . B))) * ((BS . B) * B)) is Element of the carrier of V
- ((- (1 / (BS . B))) * ((BS . B) * B)) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + (- ((- (1 / (BS . B))) * ((BS . B) * B))) is Element of the carrier of V
- (- (1 / (BS . B))) is V21() real ext-real Element of REAL
(- (- (1 / (BS . B)))) * ((BS . B) * B) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + ((- (- (1 / (BS . B)))) * ((BS . B) * B)) is Element of the carrier of V
(1 / (BS . B)) * (BS . B) is V21() real ext-real Element of REAL
((1 / (BS . B)) * (BS . B)) * B is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + (((1 / (BS . B)) * (BS . B)) * B) is Element of the carrier of V
1 * B is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + (1 * B) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + B is Element of the carrier of V
- ((1 / (BS . B)) * (Sum BS)) is Element of the carrier of V
(- ((1 / (BS . B)) * (Sum BS))) + B is Element of the carrier of V
((1 / (BS . B)) * (Sum BS)) + (- ((1 / (BS . B)) * (Sum BS))) is Element of the carrier of V
(((1 / (BS . B)) * (Sum BS)) + (- ((1 / (BS . B)) * (Sum BS)))) + B is Element of the carrier of V
((1 / (BS . B)) * (Sum BS)) - ((1 / (BS . B)) * (Sum BS)) is Element of the carrier of V
(((1 / (BS . B)) * (Sum BS)) - ((1 / (BS . B)) * (Sum BS))) + B is Element of the carrier of V
V is V21() real ext-real Element of REAL
1 - V is V21() real ext-real Element of REAL
B is V21() real ext-real Element of REAL
1 - B is V21() real ext-real Element of REAL
S is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of S is non empty set
bool the carrier of S is non empty non empty-membered set
BS is Element of the carrier of S
U is Element of the carrier of S
V * U is Element of the carrier of S
B * U is Element of the carrier of S
x is affinely-independent Element of bool the carrier of S
conv x is convex Element of bool the carrier of S
y is Element of the carrier of S
{y} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of S
x \ {y} is Element of bool the carrier of S
conv (x \ {y}) is convex Element of bool the carrier of S
X is Element of the carrier of S
{X} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of S
x \ {X} is Element of bool the carrier of S
conv (x \ {X}) is convex Element of bool the carrier of S
U is Element of the carrier of S
xBS is Element of the carrier of S
(1 - V) * U is Element of the carrier of S
(V * U) + ((1 - V) * U) is Element of the carrier of S
(1 - B) * xBS is Element of the carrier of S
(B * U) + ((1 - B) * xBS) is Element of the carrier of S
U |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
BS |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
U |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
xBS |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
Affin x is Affine Element of bool the carrier of S
(U |-- x) . X is V21() real ext-real Element of REAL
y is set
(U |-- x) . y is V21() real ext-real set
Affin (x \ {X}) is Affine Element of bool the carrier of S
xBS |-- (x \ {X}) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x \ {X}
Carrier (xBS |-- x) is finite Element of bool the carrier of S
{ b₁ where b₁ is Element of the carrier of S : not (xBS |-- x) . b₁ = 0 } is set
(xBS |-- x) . X is V21() real ext-real Element of REAL
(U |-- x) . y is V21() real ext-real Element of REAL
y is set
(U |-- x) . y is V21() real ext-real set
Affin (x \ {y}) is Affine Element of bool the carrier of S
U |-- (x \ {y}) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x \ {y}
Carrier (U |-- x) is finite Element of bool the carrier of S
{ b₁ where b₁ is Element of the carrier of S : not (U |-- x) . b₁ = 0 } is set
(U |-- x) . y is V21() real ext-real Element of REAL
B * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - B) * (xBS |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(B * (U |-- x)) + ((1 - B) * (xBS |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(BS |-- x) . X is V21() real ext-real Element of REAL
(B * (U |-- x)) . X is V21() real ext-real Element of REAL
((1 - B) * (xBS |-- x)) . X is V21() real ext-real Element of REAL
((B * (U |-- x)) . X) + (((1 - B) * (xBS |-- x)) . X) is V21() real ext-real Element of REAL
B * ((U |-- x) . X) is V21() real ext-real Element of REAL
(B * ((U |-- x) . X)) + (((1 - B) * (xBS |-- x)) . X) is V21() real ext-real Element of REAL
(1 - B) * ((xBS |-- x) . X) is V21() real ext-real Element of REAL
(B * ((U |-- x) . X)) + ((1 - B) * ((xBS |-- x) . X)) is V21() real ext-real Element of REAL
1 * ((U |-- x) . X) is V21() real ext-real Element of REAL
((BS |-- x) . X) - ((BS |-- x) . X) is V21() real ext-real Element of REAL
((U |-- x) . X) - ((BS |-- x) . X) is V21() real ext-real Element of REAL
(U |-- x) . X is V21() real ext-real Element of REAL
1 / (1 - B) is V21() real ext-real Element of REAL
((U |-- x) . X) / (((U |-- x) . X) - ((BS |-- x) . X)) is V21() real ext-real Element of REAL
(1 / (1 - B)) - (((U |-- x) . X) / (((U |-- x) . X) - ((BS |-- x) . X))) is V21() real ext-real Element of REAL
(1 / (1 - B)) - {} is V21() real ext-real Element of REAL
V * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - V) * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(V * (U |-- x)) + ((1 - V) * (U |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(BS |-- x) . y is V21() real ext-real Element of REAL
(V * (U |-- x)) . y is V21() real ext-real Element of REAL
((1 - V) * (U |-- x)) . y is V21() real ext-real Element of REAL
((V * (U |-- x)) . y) + (((1 - V) * (U |-- x)) . y) is V21() real ext-real Element of REAL
V * ((U |-- x) . y) is V21() real ext-real Element of REAL
(V * ((U |-- x) . y)) + (((1 - V) * (U |-- x)) . y) is V21() real ext-real Element of REAL
(1 - V) * ((U |-- x) . y) is V21() real ext-real Element of REAL
(V * ((U |-- x) . y)) + ((1 - V) * ((U |-- x) . y)) is V21() real ext-real Element of REAL
1 * ((U |-- x) . y) is V21() real ext-real Element of REAL
((BS |-- x) . y) - ((BS |-- x) . y) is V21() real ext-real Element of REAL
((U |-- x) . y) - ((BS |-- x) . y) is V21() real ext-real Element of REAL
(1 / (1 - B)) * BS is Element of the carrier of S
1 - (1 / (1 - B)) is V21() real ext-real Element of REAL
(1 - (1 / (1 - B))) * U is Element of the carrier of S
((1 / (1 - B)) * BS) + ((1 - (1 / (1 - B))) * U) is Element of the carrier of S
(1 / (1 - B)) * (BS |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - (1 / (1 - B))) * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((1 / (1 - B)) * (BS |-- x)) + ((1 - (1 / (1 - B))) * (U |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((U |-- x) . X) - {} is V21() real ext-real Element of REAL
(((U |-- x) . X) - {}) / (((U |-- x) . X) - ((BS |-- x) . X)) is V21() real ext-real Element of REAL
1 / (1 - V) is V21() real ext-real Element of REAL
(1 / (1 - V)) * BS is Element of the carrier of S
1 - (1 / (1 - V)) is V21() real ext-real Element of REAL
(1 - (1 / (1 - V))) * U is Element of the carrier of S
((1 / (1 - V)) * BS) + ((1 - (1 / (1 - V))) * U) is Element of the carrier of S
(1 / (1 - V)) * (BS |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - (1 / (1 - V))) * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((1 / (1 - V)) * (BS |-- x)) + ((1 - (1 / (1 - V))) * (U |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((U |-- x) . X) - ((U |-- x) . X) is V21() real ext-real Element of REAL
(((U |-- x) . X) - ((U |-- x) . X)) / (((U |-- x) . X) - ((BS |-- x) . X)) is V21() real ext-real Element of REAL
(xBS |-- x) . y is V21() real ext-real Element of REAL
((xBS |-- x) . y) / (((U |-- x) . y) - ((BS |-- x) . y)) is V21() real ext-real Element of REAL
(1 / (1 - V)) - (((xBS |-- x) . y) / (((U |-- x) . y) - ((BS |-- x) . y))) is V21() real ext-real Element of REAL
(1 / (1 - V)) - {} is V21() real ext-real Element of REAL
((U |-- x) . y) - {} is V21() real ext-real Element of REAL
(((U |-- x) . y) - {}) / (((U |-- x) . y) - ((BS |-- x) . y)) is V21() real ext-real Element of REAL
((U |-- x) . y) - ((xBS |-- x) . y) is V21() real ext-real Element of REAL
(((U |-- x) . y) - ((xBS |-- x) . y)) / (((U |-- x) . y) - ((BS |-- x) . y)) is V21() real ext-real Element of REAL
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is finite Element of bool the carrier of V
S is finite affinely-independent Element of bool the carrier of V
conv S is convex Element of bool the carrier of V
Affin S is Affine Element of bool the carrier of V
BS is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
BS + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
Affin U is Affine Element of bool the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of U
Carrier x is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not x . b₁ = 0 } is set
sum x is V21() real ext-real Element of REAL
Sum x is Element of the carrier of V
(Sum x) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of U : sum b₁ = 1 } is set
y is Element of the carrier of V
((Sum x) |-- S) . y is V21() real ext-real Element of REAL
X is set
{X} is non empty trivial finite 1 -element set
U is Element of the carrier of V
x . U is V21() real ext-real Element of REAL
U |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(U |-- S) . y is V21() real ext-real Element of REAL
<*((U |-- S) . y)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
<*U*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum <*((U |-- S) . y)*> is V21() real ext-real Element of REAL
len <*((U |-- S) . y)*> is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
dom <*((U |-- S) . y)*> is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
len <*U*> is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
rng <*U*> is Element of bool the carrier of V
(x . U) * U is Element of the carrier of V
xU is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
<*((U |-- S) . y)*> . xU is V21() real ext-real set
<*U*> . xU is set
x . (<*U*> . xU) is V21() real ext-real set
(<*U*> . xU) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((<*U*> . xU) |-- S) . y is V21() real ext-real Element of REAL
(x . (<*U*> . xU)) * (((<*U*> . xU) |-- S) . y) is V21() real ext-real Element of REAL
y is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng y is Element of bool the carrier of V
x * y is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
Sum (x * y) is V21() real ext-real Element of REAL
dom y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
card (dom y) is epsilon-transitive epsilon-connected ordinal cardinal set
len y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
Seg (len y) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
card (Seg (len y)) is epsilon-transitive epsilon-connected ordinal cardinal set
len (x * y) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
(len y) |-> 1 is Relation-like NAT -defined NAT -valued Function-like len y -element FinSequence-like V50() V51() V52() V53() Element of (len y) -tuples_on NAT
(len y) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
len ((len y) |-> 1) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
Sum ((len y) |-> 1) is V21() set
(len y) * 1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal Element of REAL
X is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
((len y) |-> 1) . X is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
(x * y) . X is V21() real ext-real set
y . X is set
x . (y . X) is V21() real ext-real set
y is Element of the carrier of V
x . y is V21() real ext-real Element of REAL
y is Element of the carrier of V
x . y is V21() real ext-real Element of REAL
1 - (x . y) is V21() real ext-real Element of REAL
{y} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of {y}
U . y is V21() real ext-real Element of REAL
x - U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- 1 is non empty V21() real ext-real non positive negative Element of REAL
(- 1) * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
x + (- U) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 / (1 - (x . y)) is V21() real ext-real Element of REAL
(1 / (1 - (x . y))) * (x - U) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
Carrier U is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not U . b₁ = 0 } is set
sum U is V21() real ext-real Element of REAL
sum (x - U) is V21() real ext-real Element of REAL
sum ((1 / (1 - (x . y))) * (x - U)) is V21() real ext-real Element of REAL
(1 / (1 - (x . y))) * (1 - (x . y)) is V21() real ext-real Element of REAL
(x - U) . y is V21() real ext-real Element of REAL
(x . y) - (U . y) is V21() real ext-real Element of REAL
Carrier (x - U) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not (x - U) . b₁ = 0 } is set
U \ {y} is finite Element of bool the carrier of V
card (U \ {y}) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
Sum U is Element of the carrier of V
(x . y) * y is Element of the carrier of V
xU is set
p is Element of the carrier of V
x . p is V21() real ext-real Element of REAL
(x - U) . p is V21() real ext-real Element of REAL
U . p is V21() real ext-real Element of REAL
(x . p) - (U . p) is V21() real ext-real Element of REAL
xU is Element of the carrier of V
((Sum x) |-- S) . xU is V21() real ext-real Element of REAL
1 * (1 - (x . y)) is V21() real ext-real Element of REAL
(1 * (1 - (x . y))) / (1 - (x . y)) is V21() real ext-real Element of REAL
Sum ((1 / (1 - (x . y))) * (x - U)) is Element of the carrier of V
Sum (x - U) is Element of the carrier of V
(1 / (1 - (x . y))) * (Sum (x - U)) is Element of the carrier of V
(1 - (x . y)) * (Sum ((1 / (1 - (x . y))) * (x - U))) is Element of the carrier of V
(1 - (x . y)) * (1 / (1 - (x . y))) is V21() real ext-real Element of REAL
((1 - (x . y)) * (1 / (1 - (x . y)))) * (Sum (x - U)) is Element of the carrier of V
((1 - (x . y)) * (Sum ((1 / (1 - (x . y))) * (x - U)))) + ((x . y) * y) is Element of the carrier of V
(Sum x) - ((x . y) * y) is Element of the carrier of V
((Sum x) - ((x . y) * y)) + ((x . y) * y) is Element of the carrier of V
U \/ {y} is non empty finite Element of bool the carrier of V
Carrier ((1 / (1 - (x . y))) * (x - U)) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not ((1 / (1 - (x . y))) * (x - U)) . b₁ = 0 } is set
(Sum ((1 / (1 - (x . y))) * (x - U))) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) . xU is V21() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
Sum p is V21() real ext-real Element of REAL
u is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len u is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
len p is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
rng u is Element of bool the carrier of V
dom p is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
(1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
y |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(x . y) * (y |-- S) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) + ((x . y) * (y |-- S)) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(1 - (x . y)) * p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
(y |-- S) . xU is V21() real ext-real Element of REAL
(x . y) * ((y |-- S) . xU) is V21() real ext-real Element of REAL
<*((x . y) * ((y |-- S) . xU))*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
((1 - (x . y)) * p) ^ <*((x . y) * ((y |-- S) . xU))*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
y is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
Sum y is V21() real ext-real Element of REAL
len y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
dom y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
<*y*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
u ^ <*y*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
x is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
rng x is Element of bool the carrier of V
Sum ((1 - (x . y)) * p) is V21() real ext-real Element of REAL
(Sum ((1 - (x . y)) * p)) + ((x . y) * ((y |-- S) . xU)) is V21() real ext-real Element of REAL
(1 - (x . y)) * (((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) . xU) is V21() real ext-real Element of REAL
((1 - (x . y)) * (((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) . xU)) + ((x . y) * ((y |-- S) . xU)) is V21() real ext-real Element of REAL
((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) . xU is V21() real ext-real Element of REAL
(((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) . xU) + ((x . y) * ((y |-- S) . xU)) is V21() real ext-real Element of REAL
((x . y) * (y |-- S)) . xU is V21() real ext-real Element of REAL
(((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) . xU) + (((x . y) * (y |-- S)) . xU) is V21() real ext-real Element of REAL
(len p) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
x is Relation-like NAT -defined REAL -valued Function-like len p -element FinSequence-like V50() V51() V52() Element of (len p) -tuples_on REAL
(1 - (x . y)) * x is Relation-like NAT -defined REAL -valued Function-like len p -element FinSequence-like V50() V51() V52() Element of (len p) -tuples_on REAL
len ((1 - (x . y)) * x) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
(len p) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
rng <*y*> is Element of bool the carrier of V
(U \ {y}) \/ {y} is non empty finite Element of bool the carrier of V
p is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
y . p is V21() real ext-real set
x . p is set
x . (x . p) is V21() real ext-real set
(x . p) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((x . p) |-- S) . xU is V21() real ext-real Element of REAL
(x . (x . p)) * (((x . p) |-- S) . xU) is V21() real ext-real Element of REAL
((1 - (x . y)) * x) . p is V21() real ext-real set
x . p is V21() real ext-real set
(1 - (x . y)) * (x . p) is V21() real ext-real Element of REAL
p . p is V21() real ext-real set
u . p is set
((1 / (1 - (x . y))) * (x - U)) . (u . p) is V21() real ext-real set
(u . p) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((u . p) |-- S) . xU is V21() real ext-real Element of REAL
(((1 / (1 - (x . y))) * (x - U)) . (u . p)) * (((u . p) |-- S) . xU) is V21() real ext-real Element of REAL
dom u is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
U . (u . p) is V21() real ext-real set
(x - U) . (u . p) is V21() real ext-real set
x . (u . p) is V21() real ext-real set
(x . (u . p)) - {} is V21() real ext-real set
(1 / (1 - (x . y))) * (x . (u . p)) is V21() real ext-real Element of REAL
((1 / (1 - (x . y))) * (x - U)) . (x . p) is V21() real ext-real set
(1 - (x . y)) * (((1 / (1 - (x . y))) * (x - U)) . (x . p)) is V21() real ext-real Element of REAL
((1 - (x . y)) * (1 / (1 - (x . y)))) * (x . (u . p)) is V21() real ext-real Element of REAL
dom ((1 - (x . y)) * p) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
sum BS is V21() real ext-real Element of REAL
Sum BS is Element of the carrier of V
(Sum BS) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
Carrier BS is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not BS . b₁ = 0 } is set
y is finite Element of bool the carrier of V
card y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
Carrier X is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0 } is set
sum X is V21() real ext-real Element of REAL
Sum X is Element of the carrier of V
(Sum X) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
{} the carrier of V is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() affinely-independent V273() V274() V275() V276() Element of bool the carrier of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
U is Element of the carrier of V
((Sum X) |-- S) . U is V21() real ext-real Element of REAL
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of Carrier BS
sum x is V21() real ext-real Element of REAL
card (Carrier BS) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
y is finite Element of bool the carrier of V
card y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
Carrier X is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0 } is set
sum X is V21() real ext-real Element of REAL
Sum X is Element of the carrier of V
(Sum X) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
U is Element of the carrier of V
((Sum X) |-- S) . U is V21() real ext-real Element of REAL
y is Element of the carrier of V
((Sum BS) |-- S) . y is V21() real ext-real Element of REAL
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of the carrier of V
{B} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
S is Element of bool the carrier of V
conv S is convex Element of bool the carrier of V
S \ {B} is Element of bool the carrier of V
conv (S \ {B}) is convex Element of bool the carrier of V
BS is Element of bool the carrier of V
conv BS is convex Element of bool the carrier of V
(conv S) /\ (conv BS) is Element of bool the carrier of V
(conv (S \ {B})) /\ (conv BS) is Element of bool the carrier of V
U is Element of bool the carrier of V
x is set
y is non empty Element of bool the carrier of V
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of y : b₁ in ConvexComb V } is set
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of y
Sum X is Element of the carrier of V
X . B is V21() real ext-real Element of REAL
Carrier X is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not X . b₁ = 0 } is set
xBS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S \ {B}
Sum xBS is Element of the carrier of V
BU is non empty Element of bool the carrier of V
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BU : b₁ in ConvexComb V } is set
conv BU is non empty convex Element of bool the carrier of V
(X . B) * B is Element of the carrier of V
1 - (X . B) is V21() real ext-real Element of REAL
1 / (X . B) is V21() real ext-real Element of REAL
(1 / (X . B)) * (Sum X) is Element of the carrier of V
1 - (1 / (X . B)) is V21() real ext-real Element of REAL
xBS is Element of the carrier of V
(1 - (X . B)) * xBS is Element of the carrier of V
((X . B) * B) + ((1 - (X . B)) * xBS) is Element of the carrier of V
(1 - (1 / (X . B))) * xBS is Element of the carrier of V
((1 / (X . B)) * (Sum X)) + ((1 - (1 / (X . B))) * xBS) is Element of the carrier of V
V is non empty RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : ( b₁ in conv B & ( for b₂ being Element of bool the carrier of V holds
( not b₂ c< B or not b₁ in conv b₂ ) ) ) } is set
BS is set
U is Element of the carrier of V
BS is Element of bool the carrier of V
U is set
x is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
y is Element of the carrier of V
S is Element of bool the carrier of V
BS is Element of bool the carrier of V
U is set
x is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
x is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
V is non empty RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
S is set
V is non empty RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
conv B is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() convex V273() V274() V275() V276() Element of bool the carrier of V
V is non empty RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
S is set
BS is set
{S} is non empty trivial finite 1 -element set
B \ {S} is Element of bool the carrier of V
conv (B \ {S}) is convex Element of bool the carrier of V
S is Element of the carrier of V
{S} is non empty trivial finite 1 -element Element of bool the carrier of V
BS is Element of bool the carrier of V
conv BS is convex Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
S is Element of bool the carrier of V
(V,S) is Element of bool the carrier of V
BS is set
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= B } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= B } is set
BS is Element of bool the carrier of V
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= BS } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= BS } is set
conv BS is convex Element of bool the carrier of V
x is set
y is set
X is Element of bool the carrier of V
(V,X) is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
BS is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
BS + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv U is convex Element of bool the carrier of V
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= U } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= U } is set
y is set
(V,U) is Element of bool the carrier of V
X is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
X is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv U is convex Element of bool the carrier of V
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= U } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= U } is set
xBS is set
BU is Element of bool the carrier of V
(V,BU) is Element of bool the carrier of V
X is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
BS is finite Element of bool the carrier of V
card BS is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv BS is convex Element of bool the carrier of V
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= BS } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= BS } is set
BS is set
U is non empty Element of bool the carrier of V
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of U : b₁ in ConvexComb V } is set
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of U
Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not x . b₁ = 0 } is set
y is non empty finite Element of bool the carrier of V
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of y : b₁ in ConvexComb V } is set
conv y is non empty convex Element of bool the carrier of V
card y is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv U is convex Element of bool the carrier of V
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= U } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= U } is set
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= y } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= y } is set
U is set
xBS is Element of bool the carrier of V
(V,xBS) is Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
{ (conv (B \ {b₁})) where b₁ is Element of the carrier of V : b₁ in B } is set
union { (conv (B \ {b₁})) where b₁ is Element of the carrier of V : b₁ in B } is set
(V,B) \/ (union { (conv (B \ {b₁})) where b₁ is Element of the carrier of V : b₁ in B } ) is set
BS is set
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= B } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= B } is set
U is set
x is Element of bool the carrier of V
(V,x) is Element of bool the carrier of V
{ (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } is set
union { (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } is set
(V,B) \/ (union { (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } ) is set
y is set
X is Element of the carrier of V
{X} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
B \ {X} is Element of bool the carrier of V
conv (B \ {X}) is convex Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
{ (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } is set
union { (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } is set
(V,B) \/ (union { (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } ) is set
{ (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } is set
union { (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } is set
(V,B) \/ (union { (conv (B \ {b₂})) where b₁ is Element of the carrier of V : b₂ in B } ) is set
BS is set
U is set
x is Element of the carrier of V
{x} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
B \ {x} is Element of bool the carrier of V
conv (B \ {x}) is convex Element of bool the carrier of V
V is set
B is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of B is non empty set
bool the carrier of B is non empty non empty-membered set
S is Element of bool the carrier of B
(B,S) is Element of bool the carrier of B
conv S is convex Element of bool the carrier of B
BS is non empty Element of bool the carrier of B
ConvexComb B is set
{ (Sum b₁) where b₁ is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS : b₁ in ConvexComb B } is set
U is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS
Sum U is Element of the carrier of B
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Sum S is Element of the carrier of V
Carrier S is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not S . b₁ = 0 } is set
BS is non empty Element of bool the carrier of V
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
ConvexComb V is set
Sum U is Element of the carrier of V
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS : b₁ in ConvexComb V } is set
conv BS is non empty convex Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is affinely-independent Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Carrier S is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not S . b₁ = 0 } is set
Sum S is Element of the carrier of V
BS is non empty Element of bool the carrier of V
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
ConvexComb V is set
Sum U is Element of the carrier of V
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS : b₁ in ConvexComb V } is set
conv BS is non empty convex Element of bool the carrier of V
Affin BS is non empty Affine Element of bool the carrier of V
sum S is V21() real ext-real Element of REAL
x is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
Affin x is Affine Element of bool the carrier of V
(Sum U) |-- x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
(Sum U) |-- B is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
S is set
BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Sum BS is Element of the carrier of V
Carrier BS is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not BS . b₁ = 0 } is set
V is V21() real ext-real Element of REAL
1 - V is V21() real ext-real Element of REAL
B is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of B is non empty set
bool the carrier of B is non empty non empty-membered set
S is Element of the carrier of B
{S} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of B
V * S is Element of the carrier of B
BS is Element of the carrier of B
U is Element of the carrier of B
(1 - V) * U is Element of the carrier of B
(V * S) + ((1 - V) * U) is Element of the carrier of B
x is affinely-independent Element of bool the carrier of B
(B,x) is Element of bool the carrier of B
x \ {S} is Element of bool the carrier of B
conv (x \ {S}) is convex Element of bool the carrier of B
(B,(x \ {S})) is Element of bool the carrier of B
conv x is convex Element of bool the carrier of B
Affin x is Affine Element of bool the carrier of B
BS |-- x is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
U |-- x is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
(1 - V) * (U |-- x) is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
S |-- x is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
V * (S |-- x) is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
((1 - V) * (U |-- x)) + (V * (S |-- x)) is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
S |-- {S} is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of {S}
Carrier (S |-- {S}) is finite Element of bool the carrier of B
{ b₁ where b₁ is Element of the carrier of B : not (S |-- {S}) . b₁ = 0 } is set
Sum (BS |-- x) is Element of the carrier of B
Carrier (BS |-- x) is finite Element of bool the carrier of B
{ b₁ where b₁ is Element of the carrier of B : not (BS |-- x) . b₁ = 0 } is set
Affin {S} is non empty Affine Element of bool the carrier of B
Affin (x \ {S}) is Affine Element of bool the carrier of B
U |-- (x \ {S}) is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x \ {S}
Carrier (U |-- (x \ {S})) is finite Element of bool the carrier of B
{ b₁ where b₁ is Element of the carrier of B : not (U |-- (x \ {S})) . b₁ = 0 } is set
y is set
X is Element of the carrier of B
(S |-- x) . X is V21() real ext-real Element of REAL
(BS |-- x) . X is V21() real ext-real Element of REAL
((1 - V) * (U |-- x)) . X is V21() real ext-real Element of REAL
(V * (S |-- x)) . X is V21() real ext-real Element of REAL
(((1 - V) * (U |-- x)) . X) + ((V * (S |-- x)) . X) is V21() real ext-real Element of REAL
V * ((S |-- x) . X) is V21() real ext-real Element of REAL
(((1 - V) * (U |-- x)) . X) + (V * ((S |-- x) . X)) is V21() real ext-real Element of REAL
(U |-- x) . X is V21() real ext-real Element of REAL
(1 - V) * ((U |-- x) . X) is V21() real ext-real Element of REAL
Sum (U |-- (x \ {S})) is Element of the carrier of B
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
0. V is V79(V) Element of the carrier of V
S is set
BS is Element of bool the carrier of V
U is finite Element of bool the carrier of V
Sum U is Element of the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
1 / (card U) is V21() real ext-real non negative Element of REAL
(1 / (card U)) * (Sum U) is Element of the carrier of V
x is non empty finite Element of bool the carrier of V
Sum x is Element of the carrier of V
card x is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
1 / (card x) is non empty V21() real ext-real positive non negative Element of REAL
(1 / (card x)) * (Sum x) is Element of the carrier of V
y is Element of bool the carrier of V
BS is Element of bool the carrier of V
U is non empty finite Element of bool the carrier of V
Sum U is Element of the carrier of V
card U is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
1 / (card U) is non empty V21() real ext-real positive non negative Element of REAL
(1 / (card U)) * (Sum U) is Element of the carrier of V
x is Element of bool the carrier of V
BS is Element of bool the carrier of V
S is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BS is non empty finite Element of bool the carrier of V
S . BS is set
Sum BS is Element of the carrier of V
card BS is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
1 / (card BS) is non empty V21() real ext-real positive non negative Element of REAL
(1 / (card BS)) * (Sum BS) is Element of the carrier of V
BS is Element of bool the carrier of V
S . BS is set
S is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BS is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
U is set
S . U is set
BS . U is set
x is non empty Element of bool the carrier of V
y is non empty finite Element of bool the carrier of V
Sum y is Element of the carrier of V
card y is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
1 / (card y) is non empty V21() real ext-real positive non negative Element of REAL
(1 / (card y)) * (Sum y) is Element of the carrier of V
x is non empty Element of bool the carrier of V
x is non empty Element of bool the carrier of V
V is V21() real ext-real Element of REAL
B is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of B is non empty set
bool the carrier of B is non empty non empty-membered set
ZeroLC B is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
S is finite Element of bool the carrier of B
Sum S is Element of the carrier of B
V * (Sum S) is Element of the carrier of B
card S is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
V * (card S) is V21() real ext-real Element of REAL
S --> V is Relation-like S -defined REAL -valued Function-like constant total quasi_total finite V50() V51() V52() Element of bool [:S,REAL:]
[:S,REAL:] is Relation-like V50() V51() V52() set
bool [:S,REAL:] is non empty set
(ZeroLC B) +* (S --> V) is Relation-like Function-like V50() V51() V52() set
dom (S --> V) is finite Element of bool S
bool S is non empty finite V39() set
dom (ZeroLC B) is Element of bool the carrier of B
dom ((ZeroLC B) +* (S --> V)) is set
the carrier of B \/ S is non empty set
rng ((ZeroLC B) +* (S --> V)) is complex-membered ext-real-membered real-membered Element of bool REAL
rng (S --> V) is finite complex-membered ext-real-membered real-membered V273() V274() V275() Element of bool REAL
rng (ZeroLC B) is complex-membered ext-real-membered real-membered Element of bool REAL
(rng (S --> V)) \/ (rng (ZeroLC B)) is complex-membered ext-real-membered real-membered Element of bool REAL
[: the carrier of B,REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [: the carrier of B,REAL:] is non empty non trivial non finite non empty-membered set
Funcs ( the carrier of B,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of B, REAL
X is Element of the carrier of B
y is finite Element of bool the carrier of B
x is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Element of Funcs ( the carrier of B,REAL)
x . X is V21() real ext-real Element of REAL
(ZeroLC B) . X is V21() real ext-real Element of REAL
X is finite Element of bool the carrier of B
y is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Carrier y is finite Element of bool the carrier of B
{ b₁ where b₁ is Element of the carrier of B : not y . b₁ = 0 } is set
X is set
y . X is V21() real ext-real set
U is Element of the carrier of B
(ZeroLC B) . U is V21() real ext-real Element of REAL
X is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
Carrier X is finite Element of bool the carrier of B
{ b₁ where b₁ is Element of the carrier of B : not X . b₁ = 0 } is set
U is set
X . U is V21() real ext-real set
(S --> V) . U is V21() real ext-real set
Sum X is Element of the carrier of B
0. B is V79(B) Element of the carrier of B
sum X is V21() real ext-real Element of REAL
Sum X is Element of the carrier of B
U is Relation-like NAT -defined the carrier of B -valued Function-like FinSequence-like FinSequence of the carrier of B
rng U is Element of bool the carrier of B
X (#) U is Relation-like NAT -defined the carrier of B -valued Function-like FinSequence-like FinSequence of the carrier of B
Sum (X (#) U) is Element of the carrier of B
xBS is set
X . xBS is V21() real ext-real set
(S --> V) . xBS is V21() real ext-real set
dom U is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
card (dom U) is epsilon-transitive epsilon-connected ordinal cardinal set
len U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
Seg (len U) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
card (Seg (len U)) is epsilon-transitive epsilon-connected ordinal cardinal set
(len U) |-> V is Relation-like NAT -defined REAL -valued Function-like len U -element FinSequence-like V50() V51() V52() Element of (len U) -tuples_on REAL
(len U) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
X * U is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
len (X * U) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
xU is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
U . xU is set
(S --> V) . (U . xU) is V21() real ext-real set
BU is Relation-like NAT -defined REAL -valued Function-like len U -element FinSequence-like V50() V51() V52() Element of (len U) -tuples_on REAL
dom BU is len U -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
BU . xU is V21() real ext-real set
X . (U . xU) is V21() real ext-real set
((len U) |-> V) . xU is V21() real ext-real set
sum X is V21() real ext-real Element of REAL
Sum ((len U) |-> V) is V21() real ext-real Element of REAL
(len U) * V is V21() real ext-real Element of REAL
len (X (#) U) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
dom (X (#) U) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
p is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
U /. p is Element of the carrier of B
U . p is set
X . (U /. p) is V21() real ext-real Element of REAL
(S --> V) . (U /. p) is V21() real ext-real set
(X (#) U) . p is set
V * (U /. p) is Element of the carrier of B
Sum U is Element of the carrier of B
V * (Sum U) is Element of the carrier of B
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is finite Element of bool the carrier of V
(V) . B is set
conv B is convex Element of bool the carrier of V
S is non empty finite Element of bool the carrier of V
Sum S is Element of the carrier of V
card S is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
1 / (card S) is non empty V21() real ext-real positive non negative Element of REAL
(1 / (card S)) * (Sum S) is Element of the carrier of V
(1 / (card S)) * (card S) is non empty V21() real ext-real positive non negative Element of REAL
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
B --> (1 / (card S)) is Relation-like non-empty B -defined REAL -valued Function-like constant total quasi_total finite V50() V51() V52() Element of bool [:B,REAL:]
[:B,REAL:] is Relation-like V50() V51() V52() set
bool [:B,REAL:] is non empty set
(ZeroLC V) +* (B --> (1 / (card S))) is Relation-like Function-like V50() V51() V52() set
BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Sum BS is Element of the carrier of V
sum BS is V21() real ext-real Element of REAL
dom (B --> (1 / (card S))) is finite Element of bool B
bool B is non empty finite V39() set
U is Element of the carrier of V
BS . U is V21() real ext-real Element of REAL
(B --> (1 / (card S))) . U is V21() real ext-real set
(ZeroLC V) . U is V21() real ext-real Element of REAL
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of S : b₁ in ConvexComb V } is set
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
bool (bool the carrier of V) is non empty non empty-membered set
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is Element of bool (bool the carrier of V)
union B is Element of bool the carrier of V
(V) .: B is Element of bool the carrier of V
conv (union B) is convex Element of bool the carrier of V
BS is set
dom (V) is Element of bool (BOOL the carrier of V)
bool (BOOL the carrier of V) is non empty set
U is set
(V) . U is set
x is non empty Element of bool the carrier of V
conv x is non empty convex Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is Element of the carrier of V
S is finite affinely-independent Element of bool the carrier of V
(V) . S is set
((V) . S) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(((V) . S) |-- S) . B is V21() real ext-real Element of REAL
card S is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
1 / (card S) is V21() real ext-real non negative Element of REAL
Sum S is Element of the carrier of V
(1 / (card S)) * (Sum S) is Element of the carrier of V
(1 / (card S)) * (card S) is V21() real ext-real non negative Element of REAL
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
S --> (1 / (card S)) is Relation-like S -defined REAL -valued Function-like constant total quasi_total finite V50() V51() V52() Element of bool [:S,REAL:]
[:S,REAL:] is Relation-like V50() V51() V52() set
bool [:S,REAL:] is non empty set
(ZeroLC V) +* (S --> (1 / (card S))) is Relation-like Function-like V50() V51() V52() set
BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
Sum BS is Element of the carrier of V
sum BS is V21() real ext-real Element of REAL
conv S is convex Element of bool the carrier of V
Affin S is Affine Element of bool the carrier of V
dom (S --> (1 / (card S))) is finite Element of bool S
bool S is non empty finite V39() set
(S --> (1 / (card S))) . B is V21() real ext-real set
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is finite affinely-independent Element of bool the carrier of V
(V) . B is set
card B is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv B is convex Element of bool the carrier of V
BS is Element of the carrier of V
BS |-- B is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
(BS |-- B) . BS is V21() real ext-real Element of REAL
1 / (card B) is V21() real ext-real non negative Element of REAL
BS is set
{BS} is non empty trivial finite 1 -element set
Sum B is Element of the carrier of V
(1 / (card B)) * (Sum B) is Element of the carrier of V
U is Element of the carrier of V
1 / 1 is non empty V21() real ext-real positive non negative Element of REAL
(1 / 1) * U is Element of the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is finite affinely-independent Element of bool the carrier of V
(V) . B is set
(V,B) is Element of bool the carrier of V
((V) . B) |-- B is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Carrier (((V) . B) |-- B) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not (((V) . B) |-- B) . b₁ = 0 } is set
BS is set
(((V) . B) |-- B) . BS is V21() real ext-real set
card B is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
1 / (card B) is V21() real ext-real non negative Element of REAL
conv B is convex Element of bool the carrier of V
Affin B is Affine Element of bool the carrier of V
Sum (((V) . B) |-- B) is Element of the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is Element of bool the carrier of V
Affin B is Affine Element of bool the carrier of V
S is finite affinely-independent Element of bool the carrier of V
(V) . S is set
((V) . S) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((V) . S) |-- B is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
x is set
y is Element of the carrier of V
(((V) . S) |-- S) . y is V21() real ext-real Element of REAL
U is finite set
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
1 / (card U) is V21() real ext-real non negative Element of REAL
Carrier (((V) . S) |-- B) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not (((V) . S) |-- B) . b₁ = 0 } is set
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is Element of the carrier of V
{B} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
S is finite Element of bool the carrier of V
S \ {B} is finite Element of bool the carrier of V
(V) . S is set
(V) /. (S \ {B}) is Element of the carrier of V
card S is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
1 / (card S) is V21() real ext-real non negative Element of REAL
1 - (1 / (card S)) is V21() real ext-real Element of REAL
(1 - (1 / (card S))) * ((V) /. (S \ {B})) is Element of the carrier of V
(1 / (card S)) * B is Element of the carrier of V
((1 - (1 / (card S))) * ((V) /. (S \ {B}))) + ((1 / (card S)) * B) is Element of the carrier of V
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of {B}
U . B is V21() real ext-real Element of REAL
Sum (S \ {B}) is Element of the carrier of V
card (S \ {B}) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
1 / (card (S \ {B})) is V21() real ext-real non negative Element of REAL
(1 / (card (S \ {B}))) * (Sum (S \ {B})) is Element of the carrier of V
(1 / (card (S \ {B}))) * (card (S \ {B})) is V21() real ext-real non negative Element of REAL
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(S \ {B}) --> (1 / (card (S \ {B}))) is Relation-like S \ {B} -defined REAL -valued Function-like constant total quasi_total finite V50() V51() V52() Element of bool [:(S \ {B}),REAL:]
[:(S \ {B}),REAL:] is Relation-like V50() V51() V52() set
bool [:(S \ {B}),REAL:] is non empty set
(ZeroLC V) +* ((S \ {B}) --> (1 / (card (S \ {B})))) is Relation-like Function-like V50() V51() V52() set
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S \ {B}
Sum x is Element of the carrier of V
sum x is V21() real ext-real Element of REAL
Sum S is Element of the carrier of V
(1 / (card S)) * (Sum S) is Element of the carrier of V
(1 / (card S)) * (card S) is V21() real ext-real non negative Element of REAL
S --> (1 / (card S)) is Relation-like S -defined REAL -valued Function-like constant total quasi_total finite V50() V51() V52() Element of bool [:S,REAL:]
[:S,REAL:] is Relation-like V50() V51() V52() set
bool [:S,REAL:] is non empty set
(ZeroLC V) +* (S --> (1 / (card S))) is Relation-like Function-like V50() V51() V52() set
y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
Sum y is Element of the carrier of V
sum y is V21() real ext-real Element of REAL
(V) . (S \ {B}) is set
(1 - (1 / (card S))) * x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((1 - (1 / (card S))) * x) + U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
X is Element of the carrier of V
y . X is V21() real ext-real Element of REAL
(((1 - (1 / (card S))) * x) + U) . X is V21() real ext-real Element of REAL
((1 - (1 / (card S))) * x) . X is V21() real ext-real Element of REAL
U . X is V21() real ext-real Element of REAL
(((1 - (1 / (card S))) * x) . X) + (U . X) is V21() real ext-real Element of REAL
x . X is V21() real ext-real Element of REAL
(1 - (1 / (card S))) * (x . X) is V21() real ext-real Element of REAL
(ZeroLC V) . X is V21() real ext-real Element of REAL
Carrier U is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not U . b₁ = 0 } is set
dom (S --> (1 / (card S))) is finite Element of bool S
bool S is non empty finite V39() set
dom ((S \ {B}) --> (1 / (card (S \ {B})))) is finite Element of bool (S \ {B})
bool (S \ {B}) is non empty finite V39() set
(S --> (1 / (card S))) . B is V21() real ext-real set
(S --> (1 / (card S))) . X is V21() real ext-real set
(S \ {B}) \/ {B} is non empty finite Element of bool the carrier of V
(card (S \ {B})) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
(card S) / (card S) is V21() real ext-real non negative set
((card S) / (card S)) - (1 / (card S)) is V21() real ext-real Element of REAL
(card S) - 1 is V21() real ext-real Element of REAL
((card S) - 1) / (card S) is V21() real ext-real Element of REAL
(card (S \ {B})) / (card S) is V21() real ext-real non negative set
(1 - (1 / (card S))) * (1 / (card (S \ {B}))) is V21() real ext-real Element of REAL
((card (S \ {B})) / (card S)) / (card (S \ {B})) is V21() real ext-real non negative set
(card (S \ {B})) / (card (S \ {B})) is V21() real ext-real non negative set
((card (S \ {B})) / (card (S \ {B}))) / (card S) is V21() real ext-real non negative set
((S \ {B}) --> (1 / (card (S \ {B})))) . X is V21() real ext-real set
dom (V) is Element of bool (BOOL the carrier of V)
bool (BOOL the carrier of V) is non empty set
Sum ((1 - (1 / (card S))) * x) is Element of the carrier of V
Sum U is Element of the carrier of V
(Sum ((1 - (1 / (card S))) * x)) + (Sum U) is Element of the carrier of V
(1 - (1 / (card S))) * (Sum x) is Element of the carrier of V
((1 - (1 / (card S))) * (Sum x)) + (Sum U) is Element of the carrier of V
((1 - (1 / (card S))) * (Sum x)) + ((1 / (card S)) * B) is Element of the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
S is finite affinely-independent Element of bool the carrier of V
conv S is convex Element of bool the carrier of V
(V,S) is Element of bool the carrier of V
BS is non empty finite affinely-independent Element of bool the carrier of V
{ b₁ where b₁ is Element of bool the carrier of V : ( b₁ c= BS & ex b₂ being set st
( b₂ in conv B & b₂ in (V,b₁) ) ) } is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
x is set
y is Element of bool the carrier of V
X is set
(V,y) is Element of bool the carrier of V
x is Element of bool (bool the carrier of V)
union x is Element of bool the carrier of V
y is Element of bool the carrier of V
conv y is convex Element of bool the carrier of V
X is set
conv BS is non empty convex Element of bool the carrier of V
{ (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= BS } is set
union { (V,b₁) where b₁ is Element of bool the carrier of V : b₁ c= BS } is set
U is set
xBS is Element of bool the carrier of V
(V,xBS) is Element of bool the carrier of V
conv xBS is convex Element of bool the carrier of V
X is set
U is set
xBS is Element of bool the carrier of V
BU is set
(V,xBS) is Element of bool the carrier of V
bool BS is non empty finite V39() non empty-membered Element of bool (bool BS)
bool BS is non empty finite V39() non empty-membered set
bool (bool BS) is non empty finite V39() non empty-membered set
X is set
U is set
xBS is Element of bool the carrier of V
(V,xBS) is Element of bool the carrier of V
BU is Element of bool the carrier of V
(V,BU) is Element of bool the carrier of V
xU is set
[:BS,(bool BS):] is Relation-like non empty finite set
bool [:BS,(bool BS):] is non empty finite V39() non empty-membered set
X is Relation-like BS -defined bool BS -valued Function-like non empty total quasi_total finite Element of bool [:BS,(bool BS):]
dom X is non empty finite Element of bool BS
U is set
X . U is set
rng X is non empty finite V39() Element of bool (bool BS)
bool (bool BS) is non empty finite V39() non empty-membered set
xBS is Element of bool the carrier of V
(V,xBS) is Element of bool the carrier of V
BU is set
xU is Element of bool the carrier of V
(V,xU) is Element of bool the carrier of V
[:BS, the carrier of V:] is Relation-like non empty set
bool [:BS, the carrier of V:] is non empty non empty-membered set
U is Relation-like BS -defined the carrier of V -valued Function-like non empty total quasi_total finite Element of bool [:BS, the carrier of V:]
rng U is non empty finite Element of bool the carrier of V
xBS is non empty finite Element of bool the carrier of V
BU is set
dom U is non empty finite Element of bool BS
xU is set
U . xU is set
X . xU is set
rng X is non empty finite V39() Element of bool (bool BS)
bool (bool BS) is non empty finite V39() non empty-membered set
p is Element of bool the carrier of V
conv xBS is non empty convex Element of bool the carrier of V
dom U is non empty finite Element of bool BS
card xBS is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
1 / (card xBS) is non empty V21() real ext-real positive non negative Element of REAL
(1 / (card xBS)) * (card xBS) is non empty V21() real ext-real positive non negative Element of REAL
(card xBS) / (card xBS) is non empty V21() real ext-real positive non negative set
Sum xBS is Element of the carrier of V
(1 / (card xBS)) * (Sum xBS) is Element of the carrier of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
xBS --> (1 / (card xBS)) is Relation-like non-empty xBS -defined REAL -valued Function-like constant non empty total quasi_total finite V50() V51() V52() Element of bool [:xBS,REAL:]
[:xBS,REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:xBS,REAL:] is non empty non trivial non finite non empty-membered set
(ZeroLC V) +* (xBS --> (1 / (card xBS))) is Relation-like Function-like V50() V51() V52() set
BU is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of xBS
Sum BU is Element of the carrier of V
sum BU is V21() real ext-real Element of REAL
(Sum BU) |-- BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
(V) . xBS is set
dom (xBS --> (1 / (card xBS))) is non empty finite Element of bool xBS
bool xBS is non empty finite V39() non empty-membered set
u is set
BU . u is V21() real ext-real set
(xBS --> (1 / (card xBS))) . u is V21() real ext-real set
Carrier BU is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not BU . b₁ = 0 } is set
u is set
BU . u is V21() real ext-real set
conv BS is non empty convex Element of bool the carrier of V
Carrier ((Sum BU) |-- BS) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not ((Sum BU) |-- BS) . b₁ = 0 } is set
u is set
((Sum BU) |-- BS) . u is V21() real ext-real set
y is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
Sum y is V21() real ext-real Element of REAL
x is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
len y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
rng x is Element of bool the carrier of V
dom y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
X . u is set
rng X is non empty finite V39() Element of bool (bool BS)
bool (bool BS) is non empty finite V39() non empty-membered set
x is Element of bool the carrier of V
(V,x) is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
U . u is set
Affin x is Affine Element of bool the carrier of V
(U . u) |-- x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
Sum ((U . u) |-- x) is Element of the carrier of V
Carrier ((U . u) |-- x) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not ((U . u) |-- x) . b₁ = 0 } is set
(U . u) |-- BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
((U . u) |-- BS) . u is V21() real ext-real set
BU . (U . u) is V21() real ext-real set
dom x is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
p is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
x . p is set
BU . (x . p) is V21() real ext-real set
(x . p) |-- BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
((x . p) |-- BS) . u is V21() real ext-real set
y . p is V21() real ext-real set
(BU . (x . p)) * (((x . p) |-- BS) . u) is V21() real ext-real set
p is set
x . p is set
y . p is V21() real ext-real set
(BU . (U . u)) * (((U . u) |-- BS) . u) is V21() real ext-real set
Affin BS is non empty Affine Element of bool the carrier of V
Sum ((Sum BU) |-- BS) is Element of the carrier of V
(V,BS) is Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
B is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
Sum B is Element of the carrier of V
sum B is V21() real ext-real Element of REAL
S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
Sum S is Element of the carrier of V
sum S is V21() real ext-real Element of REAL
Carrier B is finite Element of bool the carrier of V
bool the carrier of V is non empty non empty-membered set
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0 } is set
Carrier S is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not S . b₁ = 0 } is set
(Carrier B) \/ (Carrier S) is finite Element of bool the carrier of V
BS is Relation-like Function-like FinSequence-like set
rng BS is set
U is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
S * U is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
len (S * U) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
len U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
B * U is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
len (B * U) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
(len U) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
y is Relation-like NAT -defined REAL -valued Function-like len U -element FinSequence-like V50() V51() V52() Element of (len U) -tuples_on REAL
x is Relation-like NAT -defined REAL -valued Function-like len U -element FinSequence-like V50() V51() V52() Element of (len U) -tuples_on REAL
y - x is Relation-like NAT -defined REAL -valued Function-like len U -element FinSequence-like V50() V51() V52() Element of (len U) -tuples_on REAL
len (y - x) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
dom (y - x) is len U -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
X is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
(y - x) . X is V21() real ext-real set
U /. X is Element of the carrier of V
B . (U /. X) is V21() real ext-real Element of REAL
S . (U /. X) is V21() real ext-real Element of REAL
(B . (U /. X)) - (B . (U /. X)) is V21() real ext-real Element of REAL
(S . (U /. X)) - (B . (U /. X)) is V21() real ext-real Element of REAL
dom U is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
U . X is set
dom y is len U -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
y . X is V21() real ext-real set
S . (U . X) is V21() real ext-real set
dom x is len U -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
x . X is V21() real ext-real set
B . (U . X) is V21() real ext-real set
Sum (y - x) is V21() real ext-real Element of REAL
Sum y is V21() real ext-real Element of REAL
Sum x is V21() real ext-real Element of REAL
(Sum y) - (Sum x) is V21() real ext-real Element of REAL
(sum S) - (Sum x) is V21() real ext-real Element of REAL
(sum S) - (sum B) is V21() real ext-real Element of REAL
X is Element of the carrier of V
B . X is V21() real ext-real Element of REAL
S . X is V21() real ext-real Element of REAL
X is Element of the carrier of V
rng U is Element of bool the carrier of V
dom U is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
U is set
U . U is set
xBS is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
dom y is len U -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
(y - x) . xBS is V21() real ext-real set
y . xBS is V21() real ext-real set
x . xBS is V21() real ext-real set
(y . xBS) - (x . xBS) is V21() real ext-real set
S . X is V21() real ext-real Element of REAL
dom x is len U -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
B . X is V21() real ext-real Element of REAL
(S . X) - (B . X) is V21() real ext-real Element of REAL
X is Element of the carrier of V
rng U is Element of bool the carrier of V
B . X is V21() real ext-real Element of REAL
S . X is V21() real ext-real Element of REAL
X is Element of the carrier of V
B . X is V21() real ext-real Element of REAL
S . X is V21() real ext-real Element of REAL
V is V21() real ext-real Element of REAL
1 - V is V21() real ext-real Element of REAL
B is V21() real ext-real Element of REAL
S is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of S is non empty set
BS is Element of the carrier of S
U is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
U . BS is V21() real ext-real Element of REAL
V * U is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
x . BS is V21() real ext-real Element of REAL
(1 - V) * x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(V * U) + ((1 - V) * x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((V * U) + ((1 - V) * x)) . BS is V21() real ext-real Element of REAL
(x . BS) - B is V21() real ext-real Element of REAL
(x . BS) - (U . BS) is V21() real ext-real Element of REAL
((x . BS) - B) / ((x . BS) - (U . BS)) is V21() real ext-real Element of REAL
(V * U) . BS is V21() real ext-real Element of REAL
((1 - V) * x) . BS is V21() real ext-real Element of REAL
((V * U) . BS) + (((1 - V) * x) . BS) is V21() real ext-real Element of REAL
V * (U . BS) is V21() real ext-real Element of REAL
(V * (U . BS)) + (((1 - V) * x) . BS) is V21() real ext-real Element of REAL
- V is V21() real ext-real Element of REAL
(- V) + 1 is V21() real ext-real Element of REAL
((- V) + 1) * (x . BS) is V21() real ext-real Element of REAL
(V * (U . BS)) + (((- V) + 1) * (x . BS)) is V21() real ext-real Element of REAL
(U . BS) - (x . BS) is V21() real ext-real Element of REAL
V * ((U . BS) - (x . BS)) is V21() real ext-real Element of REAL
(V * ((U . BS) - (x . BS))) + (x . BS) is V21() real ext-real Element of REAL
V * ((x . BS) - (U . BS)) is V21() real ext-real Element of REAL
((x . BS) - B) * 1 is V21() real ext-real Element of REAL
V / 1 is V21() real ext-real Element of REAL
- ((U . BS) - (x . BS)) is V21() real ext-real Element of REAL
((x . BS) - B) / (- ((U . BS) - (x . BS))) is V21() real ext-real Element of REAL
(((x . BS) - B) / (- ((U . BS) - (x . BS)))) * ((U . BS) - (x . BS)) is V21() real ext-real Element of REAL
((((x . BS) - B) / (- ((U . BS) - (x . BS)))) * ((U . BS) - (x . BS))) + (x . BS) is V21() real ext-real Element of REAL
- ((x . BS) - B) is V21() real ext-real Element of REAL
(- ((x . BS) - B)) / ((U . BS) - (x . BS)) is V21() real ext-real Element of REAL
((- ((x . BS) - B)) / ((U . BS) - (x . BS))) * ((U . BS) - (x . BS)) is V21() real ext-real Element of REAL
(((- ((x . BS) - B)) / ((U . BS) - (x . BS))) * ((U . BS) - (x . BS))) + (x . BS) is V21() real ext-real Element of REAL
(- ((x . BS) - B)) + (x . BS) is V21() real ext-real Element of REAL
V is V21() real ext-real Element of REAL
1 - V is V21() real ext-real Element of REAL
B is V21() real ext-real Element of REAL
1 - B is V21() real ext-real Element of REAL
S is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of S is non empty set
BS is Element of the carrier of S
U is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
V * U is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
B * U is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - V) * x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(V * U) + ((1 - V) * x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((V * U) + ((1 - V) * x)) . BS is V21() real ext-real Element of REAL
(1 - B) * x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(B * U) + ((1 - B) * x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((B * U) + ((1 - B) * x)) . BS is V21() real ext-real Element of REAL
y is V21() real ext-real Element of REAL
U . BS is V21() real ext-real Element of REAL
x . BS is V21() real ext-real Element of REAL
(V * U) . BS is V21() real ext-real Element of REAL
((1 - V) * x) . BS is V21() real ext-real Element of REAL
((V * U) . BS) + (((1 - V) * x) . BS) is V21() real ext-real Element of REAL
V * (U . BS) is V21() real ext-real Element of REAL
(V * (U . BS)) + (((1 - V) * x) . BS) is V21() real ext-real Element of REAL
(1 - V) * (x . BS) is V21() real ext-real Element of REAL
(V * (U . BS)) + ((1 - V) * (x . BS)) is V21() real ext-real Element of REAL
(B * U) . BS is V21() real ext-real Element of REAL
((1 - B) * x) . BS is V21() real ext-real Element of REAL
((B * U) . BS) + (((1 - B) * x) . BS) is V21() real ext-real Element of REAL
B * (U . BS) is V21() real ext-real Element of REAL
(B * (U . BS)) + (((1 - B) * x) . BS) is V21() real ext-real Element of REAL
(1 - B) * (x . BS) is V21() real ext-real Element of REAL
(B * (U . BS)) + ((1 - B) * (x . BS)) is V21() real ext-real Element of REAL
(((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS) is V21() real ext-real Element of REAL
y - (((V * U) + ((1 - V) * x)) . BS) is V21() real ext-real Element of REAL
(y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
(((B * U) + ((1 - B) * x)) . BS) - y is V21() real ext-real Element of REAL
((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
V * (((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) is V21() real ext-real Element of REAL
B * ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) is V21() real ext-real Element of REAL
(V * (((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) + (B * ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) is V21() real ext-real Element of REAL
u is V21() real ext-real Element of REAL
u * U is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
1 - u is V21() real ext-real Element of REAL
(1 - u) * x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(u * U) + ((1 - u) * x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((u * U) + ((1 - u) * x)) . BS is V21() real ext-real Element of REAL
V * ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) is V21() real ext-real Element of REAL
(V * (((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) + (V * ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) is V21() real ext-real Element of REAL
(((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) is V21() real ext-real Element of REAL
V * ((((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) is V21() real ext-real Element of REAL
B * (((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) is V21() real ext-real Element of REAL
(B * (((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) + (B * ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) is V21() real ext-real Element of REAL
B * ((((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) is V21() real ext-real Element of REAL
((((B * U) + ((1 - B) * x)) . BS) - y) + (y - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
(((((B * U) + ((1 - B) * x)) . BS) - y) + (y - (((V * U) + ((1 - V) * x)) . BS))) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
(((V * U) + ((1 - V) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS) is V21() real ext-real Element of REAL
y * ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
(y * ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
(((V * U) + ((1 - V) * x)) . BS) * ((((B * U) + ((1 - B) * x)) . BS) - y) is V21() real ext-real Element of REAL
(((B * U) + ((1 - B) * x)) . BS) * (y - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
((((V * U) + ((1 - V) * x)) . BS) * ((((B * U) + ((1 - B) * x)) . BS) - y)) + ((((B * U) + ((1 - B) * x)) . BS) * (y - (((V * U) + ((1 - V) * x)) . BS))) is V21() real ext-real Element of REAL
(((((V * U) + ((1 - V) * x)) . BS) * ((((B * U) + ((1 - B) * x)) . BS) - y)) + ((((B * U) + ((1 - B) * x)) . BS) * (y - (((V * U) + ((1 - V) * x)) . BS)))) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
((((V * U) + ((1 - V) * x)) . BS) * ((((B * U) + ((1 - B) * x)) . BS) - y)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
((((B * U) + ((1 - B) * x)) . BS) * (y - (((V * U) + ((1 - V) * x)) . BS))) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)) is V21() real ext-real Element of REAL
(((((V * U) + ((1 - V) * x)) . BS) * ((((B * U) + ((1 - B) * x)) . BS) - y)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + (((((B * U) + ((1 - B) * x)) . BS) * (y - (((V * U) + ((1 - V) * x)) . BS))) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) is V21() real ext-real Element of REAL
((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) * (((B * U) + ((1 - B) * x)) . BS) is V21() real ext-real Element of REAL
(((((V * U) + ((1 - V) * x)) . BS) * ((((B * U) + ((1 - B) * x)) . BS) - y)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + (((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) * (((B * U) + ((1 - B) * x)) . BS)) is V21() real ext-real Element of REAL
(((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) * ((V * (U . BS)) + ((1 - V) * (x . BS))) is V21() real ext-real Element of REAL
((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) * ((B * (U . BS)) + ((1 - B) * (x . BS))) is V21() real ext-real Element of REAL
((((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) * ((V * (U . BS)) + ((1 - V) * (x . BS)))) + (((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) * ((B * (U . BS)) + ((1 - B) * (x . BS)))) is V21() real ext-real Element of REAL
u * (U . BS) is V21() real ext-real Element of REAL
((((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) * (x . BS) is V21() real ext-real Element of REAL
(u * (U . BS)) + (((((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) * (x . BS)) is V21() real ext-real Element of REAL
u * (x . BS) is V21() real ext-real Element of REAL
((u * (U . BS)) + (((((((B * U) + ((1 - B) * x)) . BS) - y) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS))) + ((y - (((V * U) + ((1 - V) * x)) . BS)) / ((((B * U) + ((1 - B) * x)) . BS) - (((V * U) + ((1 - V) * x)) . BS)))) * (x . BS))) - (u * (x . BS)) is V21() real ext-real Element of REAL
1 * (x . BS) is V21() real ext-real Element of REAL
(u * (U . BS)) + (1 * (x . BS)) is V21() real ext-real Element of REAL
((u * (U . BS)) + (1 * (x . BS))) - (u * (x . BS)) is V21() real ext-real Element of REAL
(1 - u) * (x . BS) is V21() real ext-real Element of REAL
(u * (U . BS)) + ((1 - u) * (x . BS)) is V21() real ext-real Element of REAL
((1 - u) * x) . BS is V21() real ext-real Element of REAL
(u * (U . BS)) + (((1 - u) * x) . BS) is V21() real ext-real Element of REAL
(u * U) . BS is V21() real ext-real Element of REAL
((u * U) . BS) + (((1 - u) * x) . BS) is V21() real ext-real Element of REAL
y - y is V21() real ext-real Element of REAL
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of the carrier of V
S is Element of the carrier of V
BS is Element of bool the carrier of V
conv BS is convex Element of bool the carrier of V
x is non empty Element of bool the carrier of V
conv x is non empty convex Element of bool the carrier of V
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of x : b₁ in ConvexComb V } is set
y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of x
Sum y is Element of the carrier of V
Carrier y is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not y . b₁ = 0 } is set
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of x
Sum U is Element of the carrier of V
Carrier U is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not U . b₁ = 0 } is set
(Carrier y) \/ (Carrier U) is finite Element of bool the carrier of V
BU is set
xU is Element of the carrier of V
{xU} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
BS \ {xU} is Element of bool the carrier of V
p is non empty Element of bool the carrier of V
conv (BS \ {xU}) is convex Element of bool the carrier of V
y is Element of the carrier of V
U is V21() real ext-real Element of REAL
U * S is Element of the carrier of V
1 - U is V21() real ext-real Element of REAL
(1 - U) * y is Element of the carrier of V
(U * S) + ((1 - U) * y) is Element of the carrier of V
0. V is V79(V) Element of the carrier of V
1 * y is Element of the carrier of V
(0. V) + (1 * y) is Element of the carrier of V
(0. V) + y is Element of the carrier of V
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of p
Sum u is Element of the carrier of V
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of p : b₁ in ConvexComb V } is set
{ b₁ where b₁ is V21() real ext-real Element of REAL : ex b₂ being Element of the carrier of V st
( S₁[b₂,b₁] & b₂ in (Carrier y) \/ (Carrier U) ) } is set
xU is set
p is V21() real ext-real Element of REAL
u is Element of the carrier of V
xU is Element of the carrier of V
p is V21() real ext-real Element of REAL
u is V21() real ext-real Element of REAL
p * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 - p is V21() real ext-real Element of REAL
(1 - p) * y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(p * U) + ((1 - p) * y) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((p * U) + ((1 - p) * y)) . xU is V21() real ext-real Element of REAL
y . xU is V21() real ext-real Element of REAL
U . xU is V21() real ext-real Element of REAL
u * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 - u is V21() real ext-real Element of REAL
(1 - u) * y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(u * U) + ((1 - u) * y) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((u * U) + ((1 - u) * y)) . xU is V21() real ext-real Element of REAL
(y . xU) - {} is V21() real ext-real Element of REAL
(y . xU) - (U . xU) is V21() real ext-real Element of REAL
((y . xU) - {}) / ((y . xU) - (U . xU)) is V21() real ext-real Element of REAL
sum U is V21() real ext-real Element of REAL
sum y is V21() real ext-real Element of REAL
xU is Element of the carrier of V
U . xU is V21() real ext-real Element of REAL
y . xU is V21() real ext-real Element of REAL
(y . xU) - (U . xU) is V21() real ext-real Element of REAL
(y . xU) / ((y . xU) - (U . xU)) is V21() real ext-real Element of REAL
U is V21() real ext-real Element of REAL
(y . xU) - U is V21() real ext-real Element of REAL
((y . xU) - U) / ((y . xU) - (U . xU)) is V21() real ext-real Element of REAL
(U . xU) - (U . xU) is V21() real ext-real Element of REAL
u is V21() real ext-real Element of REAL
y is Element of the carrier of V
y . y is V21() real ext-real Element of REAL
U . y is V21() real ext-real Element of REAL
u * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 - u is V21() real ext-real Element of REAL
(1 - u) * y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(u * U) + ((1 - u) * y) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((u * U) + ((1 - u) * y)) . y is V21() real ext-real Element of REAL
u is non empty finite complex-membered ext-real-membered real-membered V271() V272() V273() V274() V275() set
max u is V21() real ext-real set
x is V21() real ext-real Element of REAL
x * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 - x is V21() real ext-real Element of REAL
(1 - x) * y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(x * U) + ((1 - x) * y) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
p is Element of the carrier of V
p is Element of the carrier of V
x * S is Element of the carrier of V
(1 - x) * B is Element of the carrier of V
(x * S) + ((1 - x) * B) is Element of the carrier of V
- x is V21() real ext-real Element of REAL
(- x) / (1 - x) is V21() real ext-real Element of REAL
Sum ((x * U) + ((1 - x) * y)) is Element of the carrier of V
Sum (x * U) is Element of the carrier of V
Sum ((1 - x) * y) is Element of the carrier of V
(Sum (x * U)) + (Sum ((1 - x) * y)) is Element of the carrier of V
(x * S) + (Sum ((1 - x) * y)) is Element of the carrier of V
Ap is Element of the carrier of V
((x * U) + ((1 - x) * y)) . Ap is V21() real ext-real Element of REAL
U * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 - U is V21() real ext-real Element of REAL
(1 - U) * y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(U * U) + ((1 - U) * y) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((U * U) + ((1 - U) * y)) . Ap is V21() real ext-real Element of REAL
(U * U) . Ap is V21() real ext-real Element of REAL
((1 - U) * y) . Ap is V21() real ext-real Element of REAL
((U * U) . Ap) + (((1 - U) * y) . Ap) is V21() real ext-real Element of REAL
U . Ap is V21() real ext-real Element of REAL
U * (U . Ap) is V21() real ext-real Element of REAL
(U * (U . Ap)) + (((1 - U) * y) . Ap) is V21() real ext-real Element of REAL
1 - {} is non empty V21() real ext-real positive non negative Element of REAL
y . Ap is V21() real ext-real Element of REAL
(1 - {}) * (y . Ap) is V21() real ext-real Element of REAL
(U * (U . Ap)) + ((1 - {}) * (y . Ap)) is V21() real ext-real Element of REAL
(x * U) . Ap is V21() real ext-real Element of REAL
((1 - x) * y) . Ap is V21() real ext-real Element of REAL
((x * U) . Ap) + (((1 - x) * y) . Ap) is V21() real ext-real Element of REAL
x * (U . Ap) is V21() real ext-real Element of REAL
(x * (U . Ap)) + (((1 - x) * y) . Ap) is V21() real ext-real Element of REAL
(1 - x) * (y . Ap) is V21() real ext-real Element of REAL
(x * (U . Ap)) + ((1 - x) * (y . Ap)) is V21() real ext-real Element of REAL
LW is V21() real ext-real Element of REAL
LW * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 - LW is V21() real ext-real Element of REAL
(1 - LW) * y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(LW * U) + ((1 - LW) * y) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((LW * U) + ((1 - LW) * y)) . Ap is V21() real ext-real Element of REAL
c₂₃ is V21() real ext-real Element of REAL
c₂₄ is Element of the carrier of V
y . c₂₄ is V21() real ext-real Element of REAL
U . c₂₄ is V21() real ext-real Element of REAL
c₂₃ * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 - c₂₃ is V21() real ext-real Element of REAL
(1 - c₂₃) * y is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(c₂₃ * U) + ((1 - c₂₃) * y) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((c₂₃ * U) + ((1 - c₂₃) * y)) . c₂₄ is V21() real ext-real Element of REAL
c₂₃ is Element of the carrier of V
Carrier ((x * U) + ((1 - x) * y)) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not ((x * U) + ((1 - x) * y)) . b₁ = 0 } is set
((x * U) + ((1 - x) * y)) . p is V21() real ext-real Element of REAL
{p} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
BS \ {p} is Element of bool the carrier of V
sum ((x * U) + ((1 - x) * y)) is V21() real ext-real Element of REAL
sum (x * U) is V21() real ext-real Element of REAL
sum ((1 - x) * y) is V21() real ext-real Element of REAL
(sum (x * U)) + (sum ((1 - x) * y)) is V21() real ext-real Element of REAL
x * (sum U) is V21() real ext-real Element of REAL
(x * (sum U)) + (sum ((1 - x) * y)) is V21() real ext-real Element of REAL
x * 1 is V21() real ext-real Element of REAL
(x * 1) + (sum ((1 - x) * y)) is V21() real ext-real Element of REAL
(1 - x) * (sum y) is V21() real ext-real Element of REAL
(x * 1) + ((1 - x) * (sum y)) is V21() real ext-real Element of REAL
(1 - x) * 1 is V21() real ext-real Element of REAL
(x * 1) + ((1 - x) * 1) is V21() real ext-real Element of REAL
Ap is non empty Element of bool the carrier of V
LW is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of Ap
Sum LW is Element of the carrier of V
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of Ap : b₁ in ConvexComb V } is set
conv (BS \ {p}) is convex Element of bool the carrier of V
((- x) / (1 - x)) * S is Element of the carrier of V
1 - ((- x) / (1 - x)) is V21() real ext-real Element of REAL
(1 - ((- x) / (1 - x))) * ((x * S) + ((1 - x) * B)) is Element of the carrier of V
(((- x) / (1 - x)) * S) + ((1 - ((- x) / (1 - x))) * ((x * S) + ((1 - x) * B))) is Element of the carrier of V
1 + (- x) is V21() real ext-real Element of REAL
{} + (- x) is V21() real ext-real Element of REAL
(1 + (- x)) / (1 + (- x)) is V21() real ext-real Element of REAL
(1 - x) / (1 - x) is V21() real ext-real Element of REAL
((1 - x) / (1 - x)) - ((- x) / (1 - x)) is V21() real ext-real Element of REAL
(((1 - x) / (1 - x)) - ((- x) / (1 - x))) * ((x * S) + ((1 - x) * B)) is Element of the carrier of V
(((- x) / (1 - x)) * S) + ((((1 - x) / (1 - x)) - ((- x) / (1 - x))) * ((x * S) + ((1 - x) * B))) is Element of the carrier of V
(1 - x) - (- x) is V21() real ext-real Element of REAL
((1 - x) - (- x)) / (1 - x) is V21() real ext-real Element of REAL
(((1 - x) - (- x)) / (1 - x)) * ((x * S) + ((1 - x) * B)) is Element of the carrier of V
(((- x) / (1 - x)) * S) + ((((1 - x) - (- x)) / (1 - x)) * ((x * S) + ((1 - x) * B))) is Element of the carrier of V
1 / (1 - x) is V21() real ext-real Element of REAL
(1 / (1 - x)) * (x * S) is Element of the carrier of V
(1 / (1 - x)) * ((1 - x) * B) is Element of the carrier of V
((1 / (1 - x)) * (x * S)) + ((1 / (1 - x)) * ((1 - x) * B)) is Element of the carrier of V
(((- x) / (1 - x)) * S) + (((1 / (1 - x)) * (x * S)) + ((1 / (1 - x)) * ((1 - x) * B))) is Element of the carrier of V
(1 / (1 - x)) * x is V21() real ext-real Element of REAL
((1 / (1 - x)) * x) * S is Element of the carrier of V
(((1 / (1 - x)) * x) * S) + ((1 / (1 - x)) * ((1 - x) * B)) is Element of the carrier of V
(((- x) / (1 - x)) * S) + ((((1 / (1 - x)) * x) * S) + ((1 / (1 - x)) * ((1 - x) * B))) is Element of the carrier of V
(1 / (1 - x)) * (1 - x) is V21() real ext-real Element of REAL
((1 / (1 - x)) * (1 - x)) * B is Element of the carrier of V
(((1 / (1 - x)) * x) * S) + (((1 / (1 - x)) * (1 - x)) * B) is Element of the carrier of V
(((- x) / (1 - x)) * S) + ((((1 / (1 - x)) * x) * S) + (((1 / (1 - x)) * (1 - x)) * B)) is Element of the carrier of V
x / (1 - x) is V21() real ext-real Element of REAL
(x / (1 - x)) * 1 is V21() real ext-real Element of REAL
((x / (1 - x)) * 1) * S is Element of the carrier of V
(((x / (1 - x)) * 1) * S) + (((1 / (1 - x)) * (1 - x)) * B) is Element of the carrier of V
(((- x) / (1 - x)) * S) + ((((x / (1 - x)) * 1) * S) + (((1 / (1 - x)) * (1 - x)) * B)) is Element of the carrier of V
(x / (1 - x)) * S is Element of the carrier of V
1 * B is Element of the carrier of V
((x / (1 - x)) * S) + (1 * B) is Element of the carrier of V
(((- x) / (1 - x)) * S) + (((x / (1 - x)) * S) + (1 * B)) is Element of the carrier of V
(((- x) / (1 - x)) * S) + ((x / (1 - x)) * S) is Element of the carrier of V
((((- x) / (1 - x)) * S) + ((x / (1 - x)) * S)) + (1 * B) is Element of the carrier of V
((- x) / (1 - x)) + (x / (1 - x)) is V21() real ext-real Element of REAL
(((- x) / (1 - x)) + (x / (1 - x))) * S is Element of the carrier of V
((((- x) / (1 - x)) + (x / (1 - x))) * S) + (1 * B) is Element of the carrier of V
(- x) + x is V21() real ext-real Element of REAL
((- x) + x) / (1 - x) is V21() real ext-real Element of REAL
(((- x) + x) / (1 - x)) * S is Element of the carrier of V
((((- x) + x) / (1 - x)) * S) + (1 * B) is Element of the carrier of V
{} / (1 - x) is V21() real ext-real Element of REAL
({} / (1 - x)) * S is Element of the carrier of V
(({} / (1 - x)) * S) + B is Element of the carrier of V
0. V is V79(V) Element of the carrier of V
(0. V) + B is Element of the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
BS is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of BS is non empty set
bool the carrier of BS is non empty non empty-membered set
S is Element of bool the carrier of V
B is Element of the carrier of V
{B} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
S \/ {B} is non empty Element of bool the carrier of V
Affin S is Affine Element of bool the carrier of V
x is Element of bool the carrier of BS
U is Element of the carrier of BS
Affin x is Affine Element of bool the carrier of BS
{U} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of BS
x \/ {U} is non empty Element of bool the carrier of BS
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty non empty-membered set
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
B is Element of the carrier of V
{B} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
S is finite Element of bool the carrier of V
(V) . S is set
{((V) . S)} is non empty trivial finite 1 -element set
BS is affinely-independent Element of bool the carrier of V
BS \ {B} is Element of bool the carrier of V
(BS \ {B}) \/ {((V) . S)} is non empty set
S \ {B} is finite Element of bool the carrier of V
(BS \ {B}) \/ {B} is non empty Element of bool the carrier of V
(V) /. S is Element of the carrier of V
Sum S is Element of the carrier of V
card S is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
1 / (card S) is V21() real ext-real non negative Element of REAL
(1 / (card S)) * (Sum S) is Element of the carrier of V
dom (V) is Element of bool (BOOL the carrier of V)
bool (BOOL the carrier of V) is non empty set
Affin (BS \ {B}) is Affine Element of bool the carrier of V
(V) . (S \ {B}) is set
(V) /. (S \ {B}) is Element of the carrier of V
Affin (S \ {B}) is Affine Element of bool the carrier of V
X is V21() real ext-real Element of REAL
X / X is V21() real ext-real Element of REAL
1 / X is V21() real ext-real Element of REAL
X * (1 / X) is V21() real ext-real Element of REAL
conv (S \ {B}) is convex Element of bool the carrier of V
1 - X is V21() real ext-real Element of REAL
(1 - X) * ((V) /. (S \ {B})) is Element of the carrier of V
X * ((V) /. S) is Element of the carrier of V
((1 - X) * ((V) /. (S \ {B}))) + (X * ((V) /. S)) is Element of the carrier of V
1 - (1 / X) is V21() real ext-real Element of REAL
(1 - (1 / X)) * ((V) /. (S \ {B})) is Element of the carrier of V
((V) /. S) - ((1 - (1 / X)) * ((V) /. (S \ {B}))) is Element of the carrier of V
(1 / X) * B is Element of the carrier of V
((1 - (1 / X)) * ((V) /. (S \ {B}))) + ((1 / X) * B) is Element of the carrier of V
(((1 - (1 / X)) * ((V) /. (S \ {B}))) + ((1 / X) * B)) - ((1 - (1 / X)) * ((V) /. (S \ {B}))) is Element of the carrier of V
- ((1 - (1 / X)) * ((V) /. (S \ {B}))) is Element of the carrier of V
((V) /. S) + (- ((1 - (1 / X)) * ((V) /. (S \ {B})))) is Element of the carrier of V
- (1 - (1 / X)) is V21() real ext-real Element of REAL
(- (1 - (1 / X))) * ((V) /. (S \ {B})) is Element of the carrier of V
((- (1 - (1 / X))) * ((V) /. (S \ {B}))) + ((V) /. S) is Element of the carrier of V
1 * (((1 - X) * ((V) /. (S \ {B}))) + (X * ((V) /. S))) is Element of the carrier of V
(1 / X) * (((1 - X) * ((V) /. (S \ {B}))) + (X * ((V) /. S))) is Element of the carrier of V
X * ((1 / X) * (((1 - X) * ((V) /. (S \ {B}))) + (X * ((V) /. S)))) is Element of the carrier of V
(1 / X) * ((1 - X) * ((V) /. (S \ {B}))) is Element of the carrier of V
(1 / X) * (X * ((V) /. S)) is Element of the carrier of V
((1 / X) * ((1 - X) * ((V) /. (S \ {B})))) + ((1 / X) * (X * ((V) /. S))) is Element of the carrier of V
X * (((1 / X) * ((1 - X) * ((V) /. (S \ {B})))) + ((1 / X) * (X * ((V) /. S)))) is Element of the carrier of V
1 * ((V) /. S) is Element of the carrier of V
((1 / X) * ((1 - X) * ((V) /. (S \ {B})))) + (1 * ((V) /. S)) is Element of the carrier of V
X * (((1 / X) * ((1 - X) * ((V) /. (S \ {B})))) + (1 * ((V) /. S))) is Element of the carrier of V
((1 / X) * ((1 - X) * ((V) /. (S \ {B})))) + ((V) /. S) is Element of the carrier of V
X * (((1 / X) * ((1 - X) * ((V) /. (S \ {B})))) + ((V) /. S)) is Element of the carrier of V
(1 / X) * (1 - X) is V21() real ext-real Element of REAL
((1 / X) * (1 - X)) * ((V) /. (S \ {B})) is Element of the carrier of V
(((1 / X) * (1 - X)) * ((V) /. (S \ {B}))) + ((V) /. S) is Element of the carrier of V
X * ((((1 / X) * (1 - X)) * ((V) /. (S \ {B}))) + ((V) /. S)) is Element of the carrier of V
1 * B is Element of the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
bool (bool the carrier of V) is non empty non empty-membered set
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
S is c=-linear Element of bool (bool the carrier of V)
union S is Element of bool the carrier of V
(V) .: S is Element of bool the carrier of V
dom (V) is Element of bool (BOOL the carrier of V)
bool (BOOL the carrier of V) is non empty set
BS is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
BS + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
U is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
x is c=-linear Element of bool (bool the carrier of V)
union x is Element of bool the carrier of V
card (union x) is epsilon-transitive epsilon-connected ordinal cardinal set
(V) .: x is Element of bool the carrier of V
x is c=-linear Element of bool (bool the carrier of V)
union x is Element of bool the carrier of V
card (union x) is epsilon-transitive epsilon-connected ordinal cardinal set
(V) .: x is Element of bool the carrier of V
bool (union x) is non empty Element of bool (bool (union x))
bool (union x) is non empty set
bool (bool (union x)) is non empty non empty-membered set
{(union x)} is non empty trivial finite 1 -element Element of bool (bool the carrier of V)
x \ {(union x)} is Element of bool (bool the carrier of V)
union (x \ {(union x)}) is Element of bool the carrier of V
xBS is set
BU is Element of the carrier of V
{BU} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
(union x) \ {BU} is Element of bool the carrier of V
(V) . (union x) is set
{((V) . (union x))} is non empty trivial finite 1 -element set
((union x) \ {BU}) \/ {((V) . (union x))} is non empty set
(x \ {(union x)}) \/ {(union x)} is non empty Element of bool (bool the carrier of V)
(V) .: (x \ {(union x)}) is Element of bool the carrier of V
(V) .: {(union x)} is finite Element of bool the carrier of V
((V) .: (x \ {(union x)})) \/ ((V) .: {(union x)}) is Element of bool the carrier of V
Im ((V),(union x)) is set
((V) .: (x \ {(union x)})) \/ (Im ((V),(union x))) is set
xU is Element of the carrier of V
{xU} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
((V) .: (x \ {(union x)})) \/ {xU} is non empty Element of bool the carrier of V
card {BU} is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
(x \ {(union x)}) /\ (dom (V)) is Element of bool (BOOL the carrier of V)
p is set
(V) .: {} is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() affinely-independent V273() V274() V275() V276() Element of bool the carrier of V
U is finite set
p is finite set
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
u is affinely-independent Element of bool the carrier of V
Affin ((union x) \ {BU}) is Affine Element of bool the carrier of V
y is set
x is set
(V) . x is set
x is non empty Element of bool the carrier of V
conv x is non empty convex Element of bool the carrier of V
conv ((union x) \ {BU}) is convex Element of bool the carrier of V
Affin u is Affine Element of bool the carrier of V
BS is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
U is c=-linear Element of bool (bool the carrier of V)
union U is Element of bool the carrier of V
card (union U) is epsilon-transitive epsilon-connected ordinal cardinal set
(V) .: U is Element of bool the carrier of V
U /\ (dom (V)) is Element of bool (BOOL the carrier of V)
x is set
(V) .: {} is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() affinely-independent V273() V274() V275() V276() Element of bool the carrier of V
card (union S) is epsilon-transitive epsilon-connected ordinal cardinal set
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
bool (bool the carrier of V) is non empty non empty-membered set
BOOL the carrier of V is set
bool the carrier of V is non empty non empty-membered Element of bool (bool the carrier of V)
(bool the carrier of V) \ {{}} is Element of bool (bool the carrier of V)
(V) is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty set
S is c=-linear Element of bool (bool the carrier of V)
union S is Element of bool the carrier of V
(V) .: S is Element of bool the carrier of V
(V,((V) .: S)) is Element of bool the carrier of V
(V,(union S)) is Element of bool the carrier of V
x is set
BS is affinely-independent Element of bool the carrier of V
y is set
dom (V) is Element of bool (BOOL the carrier of V)
bool (BOOL the carrier of V) is non empty set
X is set
(V) . X is set
x |-- BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
(V,BS) is Element of bool the carrier of V
conv BS is convex Element of bool the carrier of V
U is non empty finite Element of bool the carrier of V
bool U is non empty finite V39() non empty-membered Element of bool (bool U)
bool U is non empty finite V39() non empty-membered set
bool (bool U) is non empty finite V39() non empty-membered set
BU is set
(V) . U is set
Affin BS is Affine Element of bool the carrier of V
Sum (x |-- BS) is Element of the carrier of V
Carrier (x |-- BS) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not (x |-- BS) . b₁ = 0 } is set
BU is Element of the carrier of V
(x |-- BS) . BU is V21() real ext-real Element of REAL
x |-- U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of U
conv U is non empty convex Element of bool the carrier of V
Affin U is non empty Affine Element of bool the carrier of V
conv ((V) .: S) is convex Element of bool the carrier of V
Sum (x |-- U) is Element of the carrier of V
{BU} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
BS \ {BU} is Element of bool the carrier of V
conv (BS \ {BU}) is convex Element of bool the carrier of V
((x |-- BS) . BU) * BU is Element of the carrier of V
1 - ((x |-- BS) . BU) is V21() real ext-real Element of REAL
1 / ((x |-- BS) . BU) is V21() real ext-real Element of REAL
(1 / ((x |-- BS) . BU)) * (Sum (x |-- BS)) is Element of the carrier of V
1 - (1 / ((x |-- BS) . BU)) is V21() real ext-real Element of REAL
p is Element of the carrier of V
(1 - ((x |-- BS) . BU)) * p is Element of the carrier of V
(((x |-- BS) . BU) * BU) + ((1 - ((x |-- BS) . BU)) * p) is Element of the carrier of V
(1 - (1 / ((x |-- BS) . BU))) * p is Element of the carrier of V
((1 / ((x |-- BS) . BU)) * (Sum (x |-- BS))) + ((1 - (1 / ((x |-- BS) . BU))) * p) is Element of the carrier of V
((1 - ((x |-- BS) . BU)) * p) + (((x |-- BS) . BU) * BU) is Element of the carrier of V
1 - 1 is V21() real ext-real Element of REAL
p |-- U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of U
(1 - ((x |-- BS) . BU)) * (p |-- U) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
BU |-- U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of U
((x |-- BS) . BU) * (BU |-- U) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((1 - ((x |-- BS) . BU)) * (p |-- U)) + (((x |-- BS) . BU) * (BU |-- U)) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
Carrier (x |-- U) is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not (x |-- U) . b₁ = 0 } is set
u is set
(x |-- U) . u is V21() real ext-real set
((1 - ((x |-- BS) . BU)) * (p |-- U)) . u is V21() real ext-real set
(((x |-- BS) . BU) * (BU |-- U)) . u is V21() real ext-real set
(((1 - ((x |-- BS) . BU)) * (p |-- U)) . u) + ((((x |-- BS) . BU) * (BU |-- U)) . u) is V21() real ext-real set
(BU |-- U) . u is V21() real ext-real set
((x |-- BS) . BU) * ((BU |-- U) . u) is V21() real ext-real Element of REAL
(((1 - ((x |-- BS) . BU)) * (p |-- U)) . u) + (((x |-- BS) . BU) * ((BU |-- U) . u)) is V21() real ext-real Element of REAL
(p |-- U) . u is V21() real ext-real set
(1 - ((x |-- BS) . BU)) * ((p |-- U) . u) is V21() real ext-real Element of REAL
((1 - ((x |-- BS) . BU)) * ((p |-- U) . u)) + (((x |-- BS) . BU) * ((BU |-- U) . u)) is V21() real ext-real Element of REAL
card U is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
1 / (card U) is non empty V21() real ext-real positive non negative Element of REAL