let V be RealLinearSpace; :: thesis: for A being Subset of V holds conv A = union { (Int B) where B is Subset of V : B c= A }
let A be Subset of V; :: thesis: conv A = union { (Int B) where B is Subset of V : B c= A }
defpred S1[ Nat] means for S being finite Subset of V st card S <= $1 holds
conv S = union { (Int B) where B is Subset of V : B c= S } ;
set I = { (Int B) where B is Subset of V : B c= A } ;
A1: for A being Subset of V holds union { (Int B) where B is Subset of V : B c= A } c= conv A
proof
let A be Subset of V; :: thesis: union { (Int B) where B is Subset of V : B c= A } c= conv A
set I = { (Int B) where B is Subset of V : B c= A } ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in union { (Int B) where B is Subset of V : B c= A } or y in conv A )
assume y in union { (Int B) where B is Subset of V : B c= A } ; :: thesis: y in conv A
then consider x being set such that
A2: y in x and
A3: x in { (Int B) where B is Subset of V : B c= A } by TARSKI:def 4;
consider B being Subset of V such that
A4: x = Int B and
A5: B c= A by A3;
A6: conv B c= conv A by A5, RLAFFIN1:3;
y in conv B by A2, A4, Def1;
hence y in conv A by A6; :: thesis: verum
end;
A7: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A8: S1[n] ; :: thesis: S1[n + 1]
let S be finite Subset of V; :: thesis: ( card S <= n + 1 implies conv S = union { (Int B) where B is Subset of V : B c= S } )
assume A9: card S <= n + 1 ; :: thesis: conv S = union { (Int B) where B is Subset of V : B c= S }
per cases ( card S <= n or card S = n + 1 ) by A9, NAT_1:8;
suppose card S <= n ; :: thesis: conv S = union { (Int B) where B is Subset of V : B c= S }
hence conv S = union { (Int B) where B is Subset of V : B c= S } by A8; :: thesis: verum
end;
suppose A10: card S = n + 1 ; :: thesis: conv S = union { (Int B) where B is Subset of V : B c= S }
set I = { (Int B) where B is Subset of V : B c= S } ;
A11: conv S c= union { (Int B) where B is Subset of V : B c= S }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in conv S or x in union { (Int B) where B is Subset of V : B c= S } )
assume A12: x in conv S ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }
per cases ( for A being Subset of V st A c< S holds
not x in conv A or ex A being Subset of V st
( A c< S & x in conv A ) ) ;
suppose for A being Subset of V st A c< S holds
not x in conv A ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }
then ( Int S in { (Int B) where B is Subset of V : B c= S } & x in Int S ) by A12, Def1;
hence x in union { (Int B) where B is Subset of V : B c= S } by TARSKI:def 4; :: thesis: verum
end;
suppose ex A being Subset of V st
( A c< S & x in conv A ) ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }
then consider A being Subset of V such that
A13: A c< S and
A14: x in conv A ;
A15: A c= S by A13;
then reconsider A = A as finite Subset of V ;
card A < n + 1 by A10, A13, CARD_2:48;
then card A <= n by NAT_1:13;
then conv A = union { (Int B) where B is Subset of V : B c= A } by A8;
then consider Y being set such that
A16: x in Y and
A17: Y in { (Int B) where B is Subset of V : B c= A } by A14, TARSKI:def 4;
consider B being Subset of V such that
A18: Y = Int B and
A19: B c= A by A17;
B c= S by A15, A19;
then Int B in { (Int B) where B is Subset of V : B c= S } ;
hence x in union { (Int B) where B is Subset of V : B c= S } by A16, A18, TARSKI:def 4; :: thesis: verum
end;
end;
end;
union { (Int B) where B is Subset of V : B c= S } c= conv S by A1;
hence conv S = union { (Int B) where B is Subset of V : B c= S } by A11; :: thesis: verum
end;
end;
end;
A20: S1[ 0 ]
proof
let A be finite Subset of V; :: thesis: ( card A <= 0 implies conv A = union { (Int B) where B is Subset of V : B c= A } )
set I = { (Int B) where B is Subset of V : B c= A } ;
assume card A <= 0 ; :: thesis: conv A = union { (Int B) where B is Subset of V : B c= A }
then A is empty ;
then A21: conv A is empty ;
union { (Int B) where B is Subset of V : B c= A } c= conv A by A1;
hence conv A = union { (Int B) where B is Subset of V : B c= A } by A21; :: thesis: verum
end;
A22: for n being Nat holds S1[n] from NAT_1:sch 2(A20, A7);
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (Int B) where B is Subset of V : B c= A } c= conv A
let x be object ; :: thesis: ( x in conv A implies x in union { (Int B) where B is Subset of V : B c= A } )
assume A23: x in conv A ; :: thesis: x in union { (Int B) where B is Subset of V : B c= A }
reconsider A1 = A as non empty Subset of V by A23;
conv A = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;
then consider L being Convex_Combination of A1 such that
A24: ( x = Sum L & L in ConvexComb V ) by A23;
reconsider C = Carrier L as non empty finite Subset of V by CONVEX1:21;
reconsider K = L as Linear_Combination of C by RLVECT_2:def 6;
K is convex ;
then x in { (Sum M) where M is Convex_Combination of C : M in ConvexComb V } by A24;
then A25: x in conv C by CONVEX3:5;
S1[ card C] by A22;
then x in union { (Int B) where B is Subset of V : B c= C } by A25;
then consider y being set such that
A26: x in y and
A27: y in { (Int B) where B is Subset of V : B c= C } by TARSKI:def 4;
consider B being Subset of V such that
A28: y = Int B and
A29: B c= C by A27;
C c= A by RLVECT_2:def 6;
then B c= A by A29;
then Int B in { (Int B) where B is Subset of V : B c= A } ;
hence x in union { (Int B) where B is Subset of V : B c= A } by A26, A28, TARSKI:def 4; :: thesis: verum
end;
thus union { (Int B) where B is Subset of V : B c= A } c= conv A by A1; :: thesis: verum