let V be RealLinearSpace; for v1, v2 being VECTOR of V st v1 <> v2 holds
ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
let v1, v2 be VECTOR of V; ( v1 <> v2 implies ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A )
assume A1:
v1 <> v2
; ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
consider L being Linear_Combination of {v1,v2} such that
A2:
( L . v1 = jj / 2 & L . v2 = jj / 2 )
by A1, RLVECT_4:38;
consider F being FinSequence of the carrier of V such that
A3:
( F is one-to-one & rng F = Carrier L )
and
Sum L = Sum (L (#) F)
by RLVECT_2:def 8;
deffunc H1( set ) -> set = L . (F . $1);
consider f being FinSequence such that
A4:
( len f = len F & ( for n being Nat st n in dom f holds
f . n = H1(n) ) )
from FINSEQ_1:sch 2();
( v1 in Carrier L & v2 in Carrier L )
by A2, RLVECT_2:19;
then
( Carrier L c= {v1,v2} & {v1,v2} c= Carrier L )
by RLVECT_2:def 6, ZFMISC_1:32;
then A5:
{v1,v2} = Carrier L
by XBOOLE_0:def 10;
then A6:
len F = 2
by A1, A3, FINSEQ_3:98;
then
2 in dom f
by A4, FINSEQ_3:25;
then A7:
f . 2 = L . (F . 2)
by A4;
1 in dom f
by A4, A6, FINSEQ_3:25;
then A8:
f . 1 = L . (F . 1)
by A4;
now ex L, L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of Aper cases
( F = <*v1,v2*> or F = <*v2,v1*> )
by A1, A5, A3, FINSEQ_3:99;
suppose
F = <*v1,v2*>
;
ex L, L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of Athen A9:
(
F . 1
= v1 &
F . 2
= v2 )
by FINSEQ_1:44;
then
f = <*(1 / 2),(1 / 2)*>
by A2, A4, A6, A8, A7, FINSEQ_1:44;
then
f = <*jd*> ^ <*jd*>
by FINSEQ_1:def 9;
then rng f =
(rng <*(1 / 2)*>) \/ (rng <*jd*>)
by FINSEQ_1:31
.=
{jd}
by FINSEQ_1:38
;
then reconsider f =
f as
FinSequence of
REAL by FINSEQ_1:def 4;
A10:
for
n being
Nat st
n in dom f holds
(
f . n = L . (F . n) &
f . n >= 0 )
f = <*(1 / 2),(1 / 2)*>
by A2, A4, A6, A8, A7, A9, FINSEQ_1:44;
then Sum f =
(1 / 2) + (1 / 2)
by RVSUM_1:77
.=
1
;
then reconsider L =
L as
Convex_Combination of
V by A3, A4, A10, CONVEX1:def 3;
take L =
L;
ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
for
A being non
empty Subset of
V st
{v1,v2} c= A holds
L is
Convex_Combination of
A
by A5, RLVECT_2:def 6;
hence
ex
L being
Convex_Combination of
V st
for
A being non
empty Subset of
V st
{v1,v2} c= A holds
L is
Convex_Combination of
A
;
verum end; suppose
F = <*v2,v1*>
;
ex L, L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of Athen A12:
(
F . 1
= v2 &
F . 2
= v1 )
by FINSEQ_1:44;
then
f = <*(1 / 2),(1 / 2)*>
by A2, A4, A6, A8, A7, FINSEQ_1:44;
then
f = <*jd*> ^ <*jd*>
by FINSEQ_1:def 9;
then rng f =
(rng <*(1 / 2)*>) \/ (rng <*jd*>)
by FINSEQ_1:31
.=
{jd}
by FINSEQ_1:38
;
then reconsider f =
f as
FinSequence of
REAL by FINSEQ_1:def 4;
A13:
for
n being
Nat st
n in dom f holds
(
f . n = L . (F . n) &
f . n >= 0 )
f = <*(1 / 2),(1 / 2)*>
by A2, A4, A6, A8, A7, A12, FINSEQ_1:44;
then Sum f =
(1 / 2) + (1 / 2)
by RVSUM_1:77
.=
1
;
then reconsider L =
L as
Convex_Combination of
V by A3, A4, A13, CONVEX1:def 3;
take L =
L;
ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
for
A being non
empty Subset of
V st
{v1,v2} c= A holds
L is
Convex_Combination of
A
by A5, RLVECT_2:def 6;
hence
ex
L being
Convex_Combination of
V st
for
A being non
empty Subset of
V st
{v1,v2} c= A holds
L is
Convex_Combination of
A
;
verum end; end; end;
hence
ex L being Convex_Combination of V st
for A being non empty Subset of V st {v1,v2} c= A holds
L is Convex_Combination of A
; verum