:: 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;