let V be non empty RLSStruct ; :: thesis: for F being Subset-Family of V st ( for M being Subset of V st M in F holds
M is convex ) holds
meet F is convex
let F be Subset-Family of V; :: thesis: ( ( for M being Subset of V st M in F holds
M is convex ) implies meet F is convex )
assume A1: for M being Subset of V st M in F holds
M is convex ; :: thesis: meet F is convex
per cases ( F = {} or F <> {} ) ;
suppose F = {} ; :: thesis: meet F is convex
then meet F = {} by SETFAM_1:def 1;
hence meet F is convex ; :: thesis: verum
end;
suppose A2: F <> {} ; :: thesis: meet F is convex
meet F is convex
proof
let u, v be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & u in meet F & v in meet F holds
(r * u) + ((1 - r) * v) in meet F
let r be Real; :: thesis: ( 0 < r & r < 1 & u in meet F & v in meet F implies (r * u) + ((1 - r) * v) in meet F )
assume that
A3: ( 0 < r & r < 1 ) and
A4: u in meet F and
A5: v in meet F ; :: thesis: (r * u) + ((1 - r) * v) in meet F
for M being set st M in F holds
(r * u) + ((1 - r) * v) in M
proof
let M be set ; :: thesis: ( M in F implies (r * u) + ((1 - r) * v) in M )
assume A6: M in F ; :: thesis: (r * u) + ((1 - r) * v) in M
then reconsider M = M as Subset of V ;
A7: v in M by A5, A6, SETFAM_1:def 1;
( M is convex & u in M ) by A1, A4, A6, SETFAM_1:def 1;
hence (r * u) + ((1 - r) * v) in M by A3, A7; :: thesis: verum
end;
hence (r * u) + ((1 - r) * v) in meet F by A2, SETFAM_1:def 1; :: thesis: verum
end;
hence meet F is convex ; :: thesis: verum
end;
end;