let x, y be set ; :: thesis: for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let O be non empty connected Poset; :: thesis: for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let R be array of O; :: thesis: ( [x,y] in inversions R implies ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R )
assume A1: [x,y] in inversions R ; :: thesis: ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
then A2: ( x in dom R & y in dom R & x in y & R /. x > R /. y ) by Th46;
reconsider T = R as non empty array of O by A1;
reconsider p = x, q = y as Element of dom T by A1, Th46;
set j = (R,x,y) incl ;
set k = (T,p,q) incl ;
set s = Swap (R,x,y);
set t = Swap (T,p,q);
set ws = inversions (Swap (R,x,y));
set w = inversions R;
A3: dom (Swap (T,p,q)) = dom T by FUNCT_7:99;
thus ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= inversions R :: according to XBOOLE_0:def 8 :: thesis: not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R
proof
let z, t be object ; :: according to RELAT_1:def 3 :: thesis: ( not [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,t] in inversions R )
assume [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; :: thesis: [z,t] in inversions R
then consider a, b being object such that
A4: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [z,t] = ((R,x,y) incl) . (a,b) ) by Th5;
reconsider a = a, b = b as set by TARSKI:1;
( [a,b] in inversions (Swap (R,x,y)) implies ( a in dom (Swap (R,x,y)) & b in dom (Swap (R,x,y)) & a in b ) ) by Th46;
then A5: ( a in b & a in dom T & b in dom T ) by A4, A3;
then reconsider a = a, b = b as Element of dom T ;
per cases ( ( a <> p & a <> q & b <> p & b <> q ) or ( a in p & b = p ) or ( a in p & b = q ) or ( a = p & b in q ) or ( a = p & b = q ) or ( a = p & q in b ) or ( a = q & q in b ) or ( p in a & q = b ) ) by A2, A5, Th2;
suppose A6: ( a <> p & a <> q & b <> p & b <> q ) ; :: thesis: [z,t] in inversions R
then [z,t] = [a,b] by A4, A2, Th67;
hence [z,t] in inversions R by A4, A6, Th52; :: thesis: verum
end;
suppose A7: ( a in p & b = p ) ; :: thesis: [z,t] in inversions R
then [z,t] = [a,q] by A4, A2, Th68;
hence [z,t] in inversions R by A1, A4, A7, Th53; :: thesis: verum
end;
suppose A8: ( a in p & b = q ) ; :: thesis: [z,t] in inversions R
then [z,t] = [a,p] by A4, A2, Th68;
hence [z,t] in inversions R by A1, A4, A8, Th54; :: thesis: verum
end;
suppose A9: ( a = p & b in q ) ; :: thesis: [z,t] in inversions R
then [z,t] = [a,b] by A5, A4, Th69;
hence [z,t] in inversions R by A1, A4, A9, Th55; :: thesis: verum
end;
suppose ( a = p & b = q ) ; :: thesis: [z,t] in inversions R
hence [z,t] in inversions R by A1, A4, A2, Th66; :: thesis: verum
end;
suppose A10: ( a = p & q in b ) ; :: thesis: [z,t] in inversions R
then [z,t] = [q,b] by A4, A2, Th70;
hence [z,t] in inversions R by A1, A4, A10, Th57; :: thesis: verum
end;
suppose A11: ( a = q & q in b ) ; :: thesis: [z,t] in inversions R
then [z,t] = [p,b] by A4, A2, Th70;
hence [z,t] in inversions R by A1, A4, A11, Th58; :: thesis: verum
end;
suppose A12: ( p in a & q = b ) ; :: thesis: [z,t] in inversions R
then [z,t] = [a,b] by A4, A5, Th69;
hence [z,t] in inversions R by A1, A4, A12, Th56; :: thesis: verum
end;
end;
end;
now :: thesis: ( [x,y] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) implies [x,y] in inversions (Swap (R,x,y)) )
assume [x,y] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) ; :: thesis: [x,y] in inversions (Swap (R,x,y))
then consider a, b being object such that
A13: ( [a,b] in inversions (Swap (R,x,y)) & [a,b] in dom ((R,x,y) incl) & [x,y] = ((R,x,y) incl) . (a,b) ) by Th5;
A14: ((R,x,y) incl) . (p,q) = [p,q] by A2, Th66;
reconsider a = a, b = b as set by TARSKI:1;
( [a,b] in inversions (Swap (R,x,y)) implies ( a in dom (Swap (R,x,y)) & b in dom (Swap (R,x,y)) & a in b ) ) by Th46;
then A15: ( a in b & a in dom T & b in dom T ) by A13, A3;
then reconsider a = a, b = b as Element of dom T ;
( a = p & b = q ) by A2, A13, A14, A15, Lm1;
hence [x,y] in inversions (Swap (R,x,y)) by A13; :: thesis: verum
end;
hence not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R by A1, Th51; :: thesis: verum