let X be RealLinearSpace; :: thesis: for M being Subset of X holds
( M is convex iff for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M )
let M be Subset of X; :: thesis: ( M is convex iff for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M )
hereby :: thesis: ( ( for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M ) implies M is convex )
assume A1: M is convex ; :: thesis: for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M
let u, w be Point of X; :: thesis: ( u in M & w in M implies LSeg (u,w) c= M )
assume A2: ( u in M & w in M ) ; :: thesis: LSeg (u,w) c= M
thus LSeg (u,w) c= M :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (u,w) or x in M )
assume x in LSeg (u,w) ; :: thesis: x in M
then ex r being Real st
( x = ((1 - r) * u) + (r * w) & 0 <= r & r <= 1 ) ;
hence x in M by A1, A2; :: thesis: verum
end;
end;
assume A3: for w, u being Point of X st w in M & u in M holds
LSeg (w,u) c= M ; :: thesis: M is convex
let u, w be Point of X; :: according to RLTOPSP1:def 1 :: thesis: for r being Real st 0 <= r & r <= 1 & u in M & w in M holds
(r * u) + ((1 - r) * w) in M
let r be Real; :: thesis: ( 0 <= r & r <= 1 & u in M & w in M implies (r * u) + ((1 - r) * w) in M )
assume that
A4: ( 0 <= r & r <= 1 ) and
A5: ( u in M & w in M ) ; :: thesis: (r * u) + ((1 - r) * w) in M
A6: (r * u) + ((1 - r) * w) in LSeg (w,u) by A4;
LSeg (w,u) c= M by A3, A5;
hence (r * u) + ((1 - r) * w) in M by A6; :: thesis: verum