:: The Operation of Addition of Relational Structures :: by Katarzyna Romanowicz and Adam Grabowski :: :: Received May 24, 2004 :: Copyright (c) 2004-2019 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;