:: The Properties of Product of Relational Structures :: by Artur Korni{\l}owicz :: :: Received March 27, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, LATTICES, ORDERS_2, ZFMISC_1, STRUCT_0, TARSKI, SUBSET_1, LATTICE3, RELAT_2, XXREAL_0, YELLOW_0, REWRITE1, ORDINAL2, RELAT_1, MCART_1, EQREL_1, XXREAL_2, WAYBEL_0, WAYBEL_3, RCOMP_1, WAYBEL_8, WAYBEL_6, CARD_FIL, WAYBEL11, WAYBEL_2; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, DOMAIN_1, STRUCT_0, MCART_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11; constructors DOMAIN_1, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11, WAYBEL_2, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL14, RELAT_1, XTUPLE_0; requirements SUBSET, BOOLE; begin :: On the elements of product of relational structures registration let S, T be non empty upper-bounded RelStr; cluster [:S,T:] -> upper-bounded; end; registration let S, T be non empty lower-bounded RelStr; cluster [:S,T:] -> lower-bounded; end; theorem :: YELLOW10:1 for S, T being non empty RelStr st [:S,T:] is upper-bounded holds S is upper-bounded & T is upper-bounded; theorem :: YELLOW10:2 for S, T being non empty RelStr st [:S,T:] is lower-bounded holds S is lower-bounded & T is lower-bounded; theorem :: YELLOW10:3 for S, T being upper-bounded antisymmetric non empty RelStr holds Top [:S,T:] = [Top S,Top T]; theorem :: YELLOW10:4 for S, T being lower-bounded antisymmetric non empty RelStr holds Bottom [:S,T:] = [Bottom S,Bottom T]; theorem :: YELLOW10:5 for S, T being lower-bounded antisymmetric non empty RelStr, D being Subset of [:S,T:] st [:S,T:] is complete or ex_sup_of D,[:S,T:] holds sup D = [sup proj1 D,sup proj2 D]; theorem :: YELLOW10:6 for S, T being upper-bounded antisymmetric non empty RelStr, D being Subset of [:S,T:] st [:S,T:] is complete or ex_inf_of D,[:S,T:] holds inf D = [ inf proj1 D,inf proj2 D]; theorem :: YELLOW10:7 for S, T being non empty RelStr, x, y being Element of [:S,T:] holds x is_<=_than {y} iff x`1 is_<=_than {y`1} & x`2 is_<=_than {y`2}; theorem :: YELLOW10:8 for S, T being non empty RelStr, x, y, z being Element of [:S,T:] holds x is_<=_than {y,z} iff x`1 is_<=_than {y`1,z`1} & x`2 is_<=_than {y`2,z`2 }; theorem :: YELLOW10:9 for S, T being non empty RelStr, x, y being Element of [:S,T:] holds x is_>=_than {y} iff x`1 is_>=_than {y`1} & x`2 is_>=_than {y`2}; theorem :: YELLOW10:10 for S, T being non empty RelStr, x, y, z being Element of [:S,T:] holds x is_>=_than {y,z} iff x`1 is_>=_than {y`1,z`1} & x`2 is_>=_than {y`2,z`2 }; theorem :: YELLOW10:11 for S, T being non empty antisymmetric RelStr, x, y being Element of [:S,T:] holds ex_inf_of {x,y},[:S,T:] iff ex_inf_of {x`1,y`1}, S & ex_inf_of {x `2,y`2}, T; theorem :: YELLOW10:12 for S, T being non empty antisymmetric RelStr, x, y being Element of [:S,T:] holds ex_sup_of {x,y},[:S,T:] iff ex_sup_of {x`1,y`1}, S & ex_sup_of {x `2,y`2}, T; theorem :: YELLOW10:13 for S, T being with_infima antisymmetric RelStr, x, y being Element of [:S,T:] holds (x "/\" y)`1 = x`1 "/\" y`1 & (x "/\" y)`2 = x`2 "/\" y`2; theorem :: YELLOW10:14 for S, T being with_suprema antisymmetric RelStr, x, y being Element of [:S,T:] holds (x "\/" y)`1 = x`1 "\/" y`1 & (x "\/" y)`2 = x`2 "\/" y`2; theorem :: YELLOW10:15 for S, T being with_infima antisymmetric RelStr, x1, y1 being Element of S, x2, y2 being Element of T holds [x1 "/\" y1, x2 "/\" y2] = [x1,x2 ] "/\" [y1,y2]; theorem :: YELLOW10:16 for S, T being with_suprema antisymmetric RelStr, x1, y1 being Element of S, x2, y2 being Element of T holds [x1 "\/" y1, x2 "\/" y2] = [x1,x2 ] "\/" [y1,y2]; definition let S be with_suprema with_infima antisymmetric RelStr, x, y be Element of S; redefine pred y is_a_complement_of x; symmetry; end; theorem :: YELLOW10:17 for S, T being bounded with_suprema with_infima antisymmetric RelStr, x, y being Element of [:S,T:] holds x is_a_complement_of y iff x`1 is_a_complement_of y`1 & x`2 is_a_complement_of y`2; theorem :: YELLOW10:18 for S, T being antisymmetric up-complete non empty reflexive RelStr, a, c being Element of S, b, d being Element of T st [a,b] << [c,d] holds a << c & b << d; theorem :: YELLOW10:19 for S, T being up-complete non empty Poset for a, c being Element of S, b, d being Element of T holds [a,b] << [c,d] iff a << c & b << d; theorem :: YELLOW10:20 for S, T being antisymmetric up-complete non empty reflexive RelStr, x, y being Element of [:S,T:] st x << y holds x`1 << y`1 & x`2 << y`2; theorem :: YELLOW10:21 for S, T being up-complete non empty Poset, x, y being Element of [:S,T:] holds x << y iff x`1 << y`1 & x`2 << y`2; theorem :: YELLOW10:22 for S, T being antisymmetric up-complete non empty reflexive RelStr, x being Element of [:S,T:] st x is compact holds x`1 is compact & x`2 is compact; theorem :: YELLOW10:23 for S, T being up-complete non empty Poset, x being Element of [:S,T:] st x`1 is compact & x`2 is compact holds x is compact; begin :: On the subsets of product of relational structures theorem :: YELLOW10:24 for S, T being with_infima antisymmetric RelStr, X, Y being Subset of [:S,T:] holds proj1 (X "/\" Y) = proj1 X "/\" proj1 Y & proj2 (X "/\" Y) = proj2 X "/\" proj2 Y; theorem :: YELLOW10:25 for S, T being with_suprema antisymmetric RelStr, X, Y being Subset of [:S,T:] holds proj1 (X "\/" Y) = proj1 X "\/" proj1 Y & proj2 (X "\/" Y) = proj2 X "\/" proj2 Y; theorem :: YELLOW10:26 for S, T being RelStr, X being Subset of [:S,T:] holds downarrow X c= [:downarrow proj1 X,downarrow proj2 X:]; theorem :: YELLOW10:27 for S, T being RelStr, X being Subset of S, Y being Subset of T holds [:downarrow X,downarrow Y:] = downarrow [:X,Y:]; theorem :: YELLOW10:28 for S, T being RelStr, X being Subset of [:S,T:] holds proj1 downarrow X c= downarrow proj1 X & proj2 downarrow X c= downarrow proj2 X; theorem :: YELLOW10:29 for S being RelStr, T being reflexive RelStr, X being Subset of [:S,T :] holds proj1 downarrow X = downarrow proj1 X; theorem :: YELLOW10:30 for S being reflexive RelStr, T being RelStr, X being Subset of [:S,T :] holds proj2 downarrow X = downarrow proj2 X; theorem :: YELLOW10:31 for S, T being RelStr, X being Subset of [:S,T:] holds uparrow X c= [: uparrow proj1 X,uparrow proj2 X:]; theorem :: YELLOW10:32 for S, T being RelStr, X being Subset of S, Y being Subset of T holds [:uparrow X,uparrow Y:] = uparrow [:X,Y:]; theorem :: YELLOW10:33 for S, T being RelStr, X being Subset of [:S,T:] holds proj1 uparrow X c= uparrow proj1 X & proj2 uparrow X c= uparrow proj2 X; theorem :: YELLOW10:34 for S being RelStr, T being reflexive RelStr, X being Subset of [:S,T :] holds proj1 uparrow X = uparrow proj1 X; theorem :: YELLOW10:35 for S being reflexive RelStr, T being RelStr, X being Subset of [:S,T :] holds proj2 uparrow X = uparrow proj2 X; theorem :: YELLOW10:36 for S, T being non empty RelStr, s being Element of S, t being Element of T holds [:downarrow s,downarrow t:] = downarrow [s,t]; theorem :: YELLOW10:37 for S, T being non empty RelStr, x being Element of [:S,T:] holds proj1 downarrow x c= downarrow x`1 & proj2 downarrow x c= downarrow x`2 ; theorem :: YELLOW10:38 for S being non empty RelStr, T being non empty reflexive RelStr, x being Element of [:S,T:] holds proj1 downarrow x = downarrow x`1; theorem :: YELLOW10:39 for S being non empty reflexive RelStr, T being non empty RelStr, x being Element of [:S,T:] holds proj2 downarrow x = downarrow x`2; theorem :: YELLOW10:40 for S, T being non empty RelStr, s being Element of S, t being Element of T holds [:uparrow s,uparrow t:] = uparrow [s,t]; theorem :: YELLOW10:41 for S, T being non empty RelStr, x being Element of [:S,T:] holds proj1 uparrow x c= uparrow x`1 & proj2 uparrow x c= uparrow x`2; theorem :: YELLOW10:42 for S being non empty RelStr, T being non empty reflexive RelStr, x being Element of [:S,T:] holds proj1 uparrow x = uparrow x`1; theorem :: YELLOW10:43 for S being non empty reflexive RelStr, T being non empty RelStr, x being Element of [:S,T:] holds proj2 uparrow x = uparrow x`2; theorem :: YELLOW10:44 for S, T being up-complete non empty Poset, s being Element of S, t being Element of T holds [:waybelow s,waybelow t:] = waybelow [s,t]; theorem :: YELLOW10:45 for S, T being antisymmetric up-complete non empty reflexive RelStr, x being Element of [:S,T:] holds proj1 waybelow x c= waybelow x`1 & proj2 waybelow x c= waybelow x`2; theorem :: YELLOW10:46 for S being up-complete non empty Poset, T being up-complete lower-bounded non empty Poset, x being Element of [:S,T:] holds proj1 waybelow x = waybelow x`1; theorem :: YELLOW10:47 for S being up-complete lower-bounded non empty Poset, T being up-complete non empty Poset, x being Element of [:S,T:] holds proj2 waybelow x = waybelow x`2; theorem :: YELLOW10:48 for S, T being up-complete non empty Poset, s being Element of S, t being Element of T holds [:wayabove s,wayabove t:] = wayabove [s,t]; theorem :: YELLOW10:49 for S, T being antisymmetric up-complete non empty reflexive RelStr, x being Element of [:S,T:] holds proj1 wayabove x c= wayabove x`1 & proj2 wayabove x c= wayabove x`2; theorem :: YELLOW10:50 for S, T being up-complete non empty Poset, s being Element of S, t being Element of T holds [:compactbelow s,compactbelow t:] = compactbelow [s,t]; theorem :: YELLOW10:51 for S, T being antisymmetric up-complete non empty reflexive RelStr, x being Element of [:S,T:] holds proj1 compactbelow x c= compactbelow x`1 & proj2 compactbelow x c= compactbelow x`2; theorem :: YELLOW10:52 for S being up-complete non empty Poset, T being up-complete lower-bounded non empty Poset, x being Element of [:S,T:] holds proj1 compactbelow x = compactbelow x`1; theorem :: YELLOW10:53 for S being up-complete lower-bounded non empty Poset, T being up-complete non empty Poset, x being Element of [:S,T:] holds proj2 compactbelow x = compactbelow x`2; registration let S be non empty reflexive RelStr; cluster empty -> Open for Subset of S; end; theorem :: YELLOW10:54 for S, T being antisymmetric up-complete non empty reflexive RelStr, X being Subset of [:S,T:] st X is Open holds proj1 X is Open & proj2 X is Open; theorem :: YELLOW10:55 for S, T being up-complete non empty Poset, X being Subset of S, Y being Subset of T st X is Open & Y is Open holds [:X,Y:] is Open; theorem :: YELLOW10:56 for S, T being antisymmetric up-complete non empty reflexive RelStr, X being Subset of [:S,T:] st X is inaccessible holds proj1 X is inaccessible & proj2 X is inaccessible; theorem :: YELLOW10:57 for S, T being antisymmetric up-complete non empty reflexive RelStr, X being upper Subset of S, Y being upper Subset of T st X is inaccessible & Y is inaccessible holds [:X,Y:] is inaccessible; theorem :: YELLOW10:58 for S, T being antisymmetric up-complete non empty reflexive RelStr, X being Subset of S, Y being Subset of T st [:X,Y:] is directly_closed holds (Y <> {} implies X is directly_closed) & (X <> {} implies Y is directly_closed); theorem :: YELLOW10:59 for S, T being antisymmetric up-complete non empty reflexive RelStr, X being Subset of S, Y being Subset of T st X is directly_closed & Y is directly_closed holds [:X,Y:] is directly_closed; theorem :: YELLOW10:60 for S, T being antisymmetric up-complete non empty reflexive RelStr, X being Subset of [:S,T:] st X is property(S) holds proj1 X is property(S) & proj2 X is property(S); theorem :: YELLOW10:61 for S, T being up-complete non empty Poset, X being Subset of S, Y being Subset of T st X is property(S) & Y is property(S) holds [:X,Y:] is property(S); begin :: On the products of relational structures theorem :: YELLOW10:62 for S, T being non empty reflexive RelStr st the RelStr of S = the RelStr of T & S is /\-complete holds T is /\-complete; registration let S be /\-complete non empty reflexive RelStr; cluster the RelStr of S -> /\-complete; end; registration let S, T be /\-complete non empty reflexive RelStr; cluster [:S,T:] -> /\-complete; end; theorem :: YELLOW10:63 for S, T being non empty reflexive RelStr st [:S,T:] is /\-complete holds S is /\-complete & T is /\-complete; registration let S, T be complemented bounded with_infima with_suprema antisymmetric non empty RelStr; cluster [:S,T:] -> complemented; end; theorem :: YELLOW10:64 for S, T being bounded with_infima with_suprema antisymmetric RelStr st [:S,T:] is complemented holds S is complemented & T is complemented; registration let S, T be distributive with_infima with_suprema antisymmetric non empty RelStr; cluster [:S,T:] -> distributive; end; theorem :: YELLOW10:65 for S being with_infima with_suprema antisymmetric RelStr, T being with_infima with_suprema reflexive antisymmetric RelStr st [:S,T:] is distributive holds S is distributive; theorem :: YELLOW10:66 for S being with_infima with_suprema reflexive antisymmetric RelStr, T being with_infima with_suprema antisymmetric RelStr st [:S,T:] is distributive holds T is distributive; registration let S, T be meet-continuous Semilattice; cluster [:S,T:] -> satisfying_MC; end; theorem :: YELLOW10:67 for S, T being Semilattice st [:S,T:] is meet-continuous holds S is meet-continuous & T is meet-continuous; registration let S, T be satisfying_axiom_of_approximation up-complete /\-complete non empty Poset; cluster [:S,T:] -> satisfying_axiom_of_approximation; end; registration let S, T be continuous /\-complete non empty Poset; cluster [:S,T:] -> continuous; end; theorem :: YELLOW10:68 for S, T being up-complete lower-bounded non empty Poset st [:S,T:] is continuous holds S is continuous & T is continuous; registration let S, T be satisfying_axiom_K up-complete lower-bounded sup-Semilattice; cluster [:S,T:] -> satisfying_axiom_K; end; registration let S, T be complete algebraic lower-bounded sup-Semilattice; cluster [:S,T:] -> algebraic; end; theorem :: YELLOW10:69 for S, T being lower-bounded non empty Poset st [:S,T:] is algebraic holds S is algebraic & T is algebraic; registration let S, T be arithmetic lower-bounded LATTICE; cluster [:S,T:] -> arithmetic; end; theorem :: YELLOW10:70 for S, T being lower-bounded LATTICE st [:S,T:] is arithmetic holds S is arithmetic & T is arithmetic;