let V be RealLinearSpace; :: thesis: for Ks being simplex-join-closed SimplicialComplex of V
for As, Bs being Subset of Ks st As is simplex-like & @ As is affinely-independent & Bs is simplex-like holds
( Int (@ As) c= conv (@ Bs) iff As c= Bs )
let Ks be simplex-join-closed SimplicialComplex of V; :: thesis: for As, Bs being Subset of Ks st As is simplex-like & @ As is affinely-independent & Bs is simplex-like holds
( Int (@ As) c= conv (@ Bs) iff As c= Bs )
let As, Bs be Subset of Ks; :: thesis: ( As is simplex-like & @ As is affinely-independent & Bs is simplex-like implies ( Int (@ As) c= conv (@ Bs) iff As c= Bs ) )
assume that
A1: As is simplex-like and
A2: @ As is affinely-independent and
A3: Bs is simplex-like ; :: thesis: ( Int (@ As) c= conv (@ Bs) iff As c= Bs )
As in the topology of Ks by A1;
then A4: not Ks is void by PENCIL_1:def 4;
per cases ( As is empty or not As is empty ) ;
suppose A5: As is empty ; :: thesis: ( Int (@ As) c= conv (@ Bs) iff As c= Bs )
thus ( Int (@ As) c= conv (@ Bs) iff As c= Bs ) by A5; :: thesis: verum
end;
suppose not As is empty ; :: thesis: ( Int (@ As) c= conv (@ Bs) iff As c= Bs )
then not Int (@ As) is empty by A1, A2, A4, RLAFFIN2:20;
then consider x being object such that
A6: x in Int (@ As) ;
hereby :: thesis: ( As c= Bs implies Int (@ As) c= conv (@ Bs) )
assume Int (@ As) c= conv (@ Bs) ; :: thesis: As c= Bs
then x in conv (@ Bs) by A6;
then x in union { (Int b) where b is Subset of V : b c= @ Bs } by RLAFFIN2:8;
then consider Ib being set such that
A7: x in Ib and
A8: Ib in { (Int b) where b is Subset of V : b c= @ Bs } by TARSKI:def 4;
consider b being Subset of V such that
A9: Ib = Int b and
A10: b c= @ Bs by A8;
reconsider b1 = b as Subset of Ks by A10, XBOOLE_1:1;
A11: b1 is simplex-like by A3, A4, A10, MATROID0:1;
Int (@ As) meets Int (@ b1) by A6, A7, A9, XBOOLE_0:3;
hence As c= Bs by A1, A10, A11, Th25; :: thesis: verum
end;
assume As c= Bs ; :: thesis: Int (@ As) c= conv (@ Bs)
then ( Int (@ As) c= conv (@ As) & conv (@ As) c= conv (@ Bs) ) by RLAFFIN1:3, RLAFFIN2:5;
hence Int (@ As) c= conv (@ Bs) ; :: thesis: verum
end;
end;