:: The Operation of Addition of Relational Structures
:: by Katarzyna Romanowicz and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-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, ORDERS_2, PARTFUN1, STRUCT_0, FINSEQ_1, RELAT_1,
TARSKI, RELAT_2, SUBSET_1, XXREAL_0, LATTICE3, WAYBEL_0, EQREL_1,
LATTICES;
notations XBOOLE_0, TARSKI, SUBSET_1, RELSET_1, RELAT_2, STRUCT_0, ORDERS_2,
YELLOW_0, WAYBEL_0, LATTICE3;
constructors LATTICE3, WAYBEL_0, RELSET_1;
registrations XBOOLE_0, RELSET_1, STRUCT_0, WAYBEL_0;
requirements SUBSET, BOOLE;
begin
theorem :: LATSUM_1:1
for x, y, A, B being set st x in A \/ B & y in A \/ B holds x in A \ B
& y in A \ B or x in B & y in B or x in A \ B & y in B or x in B & y in A \ B
;
definition
let R, S be RelStr;
pred R tolerates S means
:: LATSUM_1:def 1
for x, y being set st x in (the carrier of R
) /\ (the carrier of S) & y in (the carrier of R) /\ (the carrier of S) holds [
x, y] in the InternalRel of R iff [x,y] in the InternalRel of S;
end;
begin
definition
let R, S be RelStr; :: Wronski Sum Operation
func R [*] S -> strict RelStr means
:: LATSUM_1:def 2
the carrier of it = (the carrier
of R) \/ (the carrier of S) & the InternalRel of it = (the InternalRel of R) \/
(the InternalRel of S) \/ ((the InternalRel of R) * the InternalRel of S);
end;
registration
let R be RelStr, S be non empty RelStr;
cluster R [*] S -> non empty;
end;
registration
let R be non empty RelStr, S be RelStr;
cluster R [*] S -> non empty;
end;
theorem :: LATSUM_1:2
for R, S being RelStr holds the InternalRel of R c= the
InternalRel of R [*] S & the InternalRel of S c= the InternalRel of R [*] S;
theorem :: LATSUM_1:3
for R, S being RelStr st R is reflexive & S is reflexive holds R
[*] S is reflexive;
begin
theorem :: LATSUM_1:4 :: theorem 3.1 (vii)
for R, S being RelStr, a, b being set st [a,b] in the InternalRel
of R [*] S & a in the carrier of R & b in the carrier of R & R tolerates S & R
is transitive holds [a,b] in the InternalRel of R;
theorem :: LATSUM_1:5 :: theorem 3.1 (viii)
for R, S being RelStr, a, b being set st [a,b] in the InternalRel
of R [*] S & a in the carrier of S & b in the carrier of S & R tolerates S & S
is transitive holds [a,b] in the InternalRel of S;
theorem :: LATSUM_1:6 :: a version of 3.1 (vii, viii - left to right)
for R, S being RelStr, a, b being object holds ([a,b] in the
InternalRel of R implies [a,b] in the InternalRel of R [*] S) & ([a,b] in the
InternalRel of S implies [a,b] in the InternalRel of R [*] S);
theorem :: LATSUM_1:7
for R, S being non empty RelStr, x being Element of R [*] S holds x in
the carrier of R or x in (the carrier of S) \ (the carrier of R);
theorem :: LATSUM_1:8 :: theorem 3.1 (vii)
for R, S being non empty RelStr for x, y being Element of R, a, b
being Element of R [*] S st x = a & y = b & R tolerates S & R is transitive
holds x <= y iff a <= b;
theorem :: LATSUM_1:9 :: theorem 3.1 (viii)
for R, S being non empty RelStr, a, b being Element of R [*] S, c
, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
a <= b iff c <= d;
theorem :: LATSUM_1:10
for R, S being antisymmetric reflexive transitive with_suprema
non empty RelStr for x being set st x in the carrier of R holds x is Element
of R [*] S;
theorem :: LATSUM_1:11
for R, S being antisymmetric reflexive transitive with_suprema non
empty RelStr for x being set st x in the carrier of S holds x is Element of R
[*] S;
theorem :: LATSUM_1:12
for R, S being non empty RelStr for x being set st x in (the
carrier of R) /\ (the carrier of S) holds x is Element of R;
theorem :: LATSUM_1:13
for R, S being non empty RelStr for x being set st x in (the
carrier of R) /\ (the carrier of S) holds x is Element of S;
theorem :: LATSUM_1:14
for R, S being antisymmetric reflexive transitive with_suprema non
empty RelStr for x, y being Element of R [*] S st x in the carrier of R & y in
the carrier of S & R tolerates S holds x <= y iff (ex a being Element of R [*]
S st a in (the carrier of R) /\ (the carrier of S) & x <= a & a <= y);
theorem :: LATSUM_1:15
for R, S being non empty RelStr, a, b being Element of R, c, d
being Element of S st a = c & b = d & R tolerates S & R is transitive & S is
transitive holds a <= b iff c <= d;
theorem :: LATSUM_1:16
for R being antisymmetric reflexive transitive with_suprema non
empty RelStr, D being lower directed Subset of R for x, y being Element of R
st x in D & y in D holds x "\/" y in D;
theorem :: LATSUM_1:17
for R, S being RelStr, a, b being set st (the carrier of R) /\ (
the carrier of S) is upper Subset of R & [a,b] in the InternalRel of R [*] S &
a in the carrier of S holds b in the carrier of S;
theorem :: LATSUM_1:18 :: theorem 3.1 (xi)
for R, S being RelStr, a, b being Element of R [*] S st (the
carrier of R) /\ (the carrier of S) is upper Subset of R & a <= b & a in the
carrier of S holds b in the carrier of S;
theorem :: LATSUM_1:19 :: theorem 3.1 (vi)
for R, S being antisymmetric reflexive transitive with_suprema non
empty RelStr for x, y being Element of R, a, b being Element of S st (the
carrier of R) /\ (the carrier of S) is lower directed Subset of S & (the
carrier of R) /\ (the carrier of S) is upper Subset of R & R tolerates S & x =
a & y = b holds x "\/" y = a "\/" b;
theorem :: LATSUM_1:20
for R, S being lower-bounded antisymmetric reflexive transitive
with_suprema non empty RelStr st (the carrier of R) /\ (the carrier of S) is
non empty lower directed Subset of S holds Bottom S in the carrier of R;
theorem :: LATSUM_1:21
for R, S being RelStr, a, b being set st (the carrier of R) /\ (
the carrier of S) is lower Subset of S & [a,b] in the InternalRel of R [*] S &
b in the carrier of R holds a in the carrier of R;
theorem :: LATSUM_1:22 :: theorem 1 (ix)
for x, y being set, R, S being RelStr st [x,y] in the InternalRel of R
[*] S & (the carrier of R) /\ (the carrier of S) is upper Subset of R holds x
in the carrier of R & y in the carrier of R or x in the carrier of S & y in the
carrier of S or x in (the carrier of R) \ (the carrier of S) & y in (the
carrier of S) \ (the carrier of R);
theorem :: LATSUM_1:23 :: theorem 3.1 (x)
for R, S being RelStr, a, b being Element of R [*] S st (the carrier
of R) /\ (the carrier of S) is lower Subset of S & a <= b & b in the carrier of
R holds a in the carrier of R;
theorem :: LATSUM_1:24 :: theorem 3.1 (xii)
for R, S being RelStr st R tolerates S & (the carrier of R) /\ (the
carrier of S) is upper Subset of R & (the carrier of R) /\ (the carrier of S)
is lower Subset of S & R is transitive antisymmetric & S is transitive
antisymmetric holds R [*] S is antisymmetric;
theorem :: LATSUM_1:25 :: theorem 3.1 (xiii)
for R, S being RelStr st (the carrier of R) /\ (the carrier of S) is
upper Subset of R & (the carrier of R) /\ (the carrier of S) is lower Subset of
S & R tolerates S & R is transitive & S is transitive holds R [*] S is
transitive;