:: Many-Argument Relations
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990-2026 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 SUBSET_1, NUMBERS, XBOOLE_0, FUNCOP_1, FUNCT_2, RELAT_1, TARSKI,
FINSEQ_1, CARD_3, FUNCT_1, ZFMISC_1, ORDINAL4, CARD_1, XBOOLEAN,
MARGREL1, PARTFUN1, NAT_1, UNIALG_1, FINSEQ_2, UNIALG_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1,
RELAT_1, NAT_1, PARTFUN1, FUNCT_2, XBOOLEAN, CARD_3, FINSEQ_1, FINSEQ_2,
FUNCOP_1;
constructors FUNCOP_1, XCMPLX_0, FINSEQ_1, XBOOLEAN, RELSET_1, CARD_3,
FINSEQ_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XBOOLEAN, FINSEQ_1,
FINSEQ_2, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, CARD_1, CARD_3,
FUNCT_2;
requirements SUBSET, BOOLE, ARITHM, NUMERALS;
definitions TARSKI, XBOOLE_0, FINSEQ_1, CARD_3, FUNCT_1;
equalities XBOOLEAN, FINSEQ_1, FUNCOP_1, ORDINAL1;
expansions TARSKI, XBOOLEAN, CARD_3, FUNCT_1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FUNCT_2, FUNCOP_1, XBOOLE_1, XBOOLEAN,
FUNCT_1, CARD_3, FINSEQ_3, RELAT_1, RELSET_1, PARTFUN1, ORDINAL1,
FINSEQ_2;
schemes XBOOLE_0, FUNCT_1;
begin
reserve x,z for set;
reserve k for Element of NAT;
reserve D for non empty set;
definition
let IT be FinSequence-membered set;
redefine attr IT is with_common_domain means :: redefines with_common_domain (CARD_3, definition)
:Def1:
for a,b being FinSequence st a in IT & b in IT holds len a = len b;
compatibility
proof
thus IT is with_common_domain implies
for a,b being FinSequence st a in IT & b in IT holds len a = len b
proof
assume
A1: IT is with_common_domain;
let a,b being FinSequence;
assume a in IT & b in IT;
then dom a = dom b by A1;
hence len a = len b by FINSEQ_3:29;
end;
assume
A2: for a,b being FinSequence st a in IT & b in IT holds len a = len b;
let f,g be Function;
assume
A3: f in IT & g in IT;
then reconsider f,g as FinSequence;
len f = len g by A2,A3;
hence thesis by FINSEQ_3:29;
end;
end;
registration
cluster FinSequence-membered with_common_domain for set;
existence
proof
take {};
thus thesis;
end;
end;
definition
mode relation is FinSequence-membered with_common_domain set;
end;
reserve X for set;
reserve p,r for relation;
reserve a,a1,a2,b for FinSequence;
theorem
X c= p implies X is relation;
theorem
{a} is relation
proof
for z being object st z in {a} holds z is FinSequence by TARSKI:def 1;
then reconsider X ={a} as FinSequence-membered set by FINSEQ_1:def 19;
X is with_common_domain;
hence thesis;
end;
scheme
relexist{A() -> set, P[FinSequence]}:
ex r st for a holds a in r iff a in A() & P[a]
provided
A1: for a,b st P[a] & P[b] holds len a = len b
proof
defpred P1[object] means ex a st P[a] & $1 = a;
consider X such that
A2: for x being object holds x in X iff x in A() & P1[x] from XBOOLE_0:sch 1;
X is FinSequence-membered
proof
let x be object;
assume x in X;
then ex a st P[a] & x = a by A2;
hence thesis;
end;
then reconsider X as FinSequence-membered set;
X is with_common_domain
proof
let a,b;
assume that
A3: a in X and
A4: b in X;
A5: ex d being FinSequence st P[d] & b = d by A2,A4;
ex c being FinSequence st P[c] & a = c by A2,A3;
hence thesis by A1,A5;
end;
then reconsider r = X as relation;
for a holds a in r iff a in A() & P[a]
proof
let a;
now
assume
A6: a in r;
then ex c being FinSequence st P[c] & a = c by A2;
hence a in A() & P[a] by A2,A6;
end;
hence thesis by A2;
end;
hence thesis;
end;
definition
let p,r;
redefine pred p = r means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for a holds a in p iff a in r;
compatibility
proof
thus p = r implies for a holds a in p iff a in r;
assume for a holds a in p iff a in r;
then for x being object holds x in p iff x in r;
hence thesis by TARSKI:2;
end;
end;
registration
cluster empty -> with_common_domain for set;
coherence;
end;
theorem
for p st for a holds not a in p holds p = {};
definition
let p;
assume
A1: p <> {};
func the_arity_of p -> Element of NAT means
for a st a in p holds it = len a;
existence
proof
consider c being FinSequence such that
A2: c in p by A1;
for a st a in p holds len c = len a by A2,Def1;
hence thesis;
end;
uniqueness
proof
let n1,n2 be Element of NAT;
assume that
A3: for a st a in p holds n1 = len a and
A4: for a st a in p holds n2 = len a;
consider a such that
A5: a in p by A1;
len a = n1 by A3,A5;
hence thesis by A4,A5;
end;
end;
definition
let k;
mode relation_length of k -> relation means
for a st a in it holds len a = k;
existence
proof
take {};
thus thesis;
end;
end;
definition
let X be set;
mode relation of X -> relation means
for a st a in it holds rng a c= X;
existence
proof
take {};
thus thesis;
end;
end;
theorem Th4:
{} is relation of X
proof
thus a in {} implies rng a c= X;
end;
theorem Th5:
{} is relation_length of k
proof
thus a in {} implies len a = k;
end;
definition
let X, k;
mode relation of X,k -> relation means
it is relation of X & it is relation_length of k;
existence
proof
take {};
thus thesis by Th4,Th5;
end;
end;
definition
let D;
func relations_on D -> set means
:Def7:
for X holds X in it iff X c= D* &
for a,b being FinSequence of D st a in X & b in X holds len a = len b;
existence
proof
defpred P[object] means
ex Y being set st Y = $1 & Y c= D* & for a,b being
FinSequence of D st a in Y & b in Y holds len a = len b;
consider A being set such that
A1: for x being object holds x in A iff x in bool(D*) & P[x]
from XBOOLE_0:sch 1;
take A;
for X being set holds X in A iff X c= D* & for a,b being FinSequence
of D st a in X & b in X holds len a = len b
proof
let X be set;
thus X in A implies X c= D* & for a,b being FinSequence of D st a in X &
b in X holds len a = len b
proof
assume X in A;
then
ex Y being set st Y = X & Y c= D* & for a,b being FinSequence of D
st a in Y & b in Y holds len a=len b by A1;
hence thesis;
end;
thus thesis by A1;
end;
hence thesis;
end;
uniqueness
proof
let A1,A2 be set;
assume that
A2: for X being set holds X in A1 iff X c= D* & for a,b being
FinSequence of D st a in X & b in X holds len a=len b and
A3: for X being set holds X in A2 iff X c= D* & for a,b being
FinSequence of D st a in X & b in X holds len a=len b;
for x being object holds x in A1 iff x in A2
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
thus x in A1 implies x in A2
proof
assume
A4: x in A1;
then
A5: for a,b being FinSequence of D st a in xx & b in xx holds len a=len
b by A2;
xx c= D* by A2,A4;
hence thesis by A3,A5;
end;
thus x in A2 implies x in A1
proof
assume
A6: x in A2;
then
A7: for a,b being FinSequence of D st a in xx & b in xx holds len a=len
b by A3;
xx c= D* by A3,A6;
hence thesis by A2,A7;
end;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let D;
cluster relations_on D -> non empty;
coherence
proof
A1: for a,b being FinSequence of D st a in {} & b in {} holds len a = len b;
defpred P[object] means
ex Y being set st Y = $1 & Y c= D* & for a,b being
FinSequence of D st a in Y & b in Y holds len a = len b;
consider XX being set such that
A2: for x being object
holds x in XX iff x in bool(D*) & P[x] from XBOOLE_0:sch 1;
{} c= D*;
then reconsider A = XX as non empty set by A2,A1;
for X being set holds X in A iff X c= D* & for a,b being FinSequence
of D st a in X & b in X holds len a = len b
proof
let X be set;
thus X in A implies X c= D* & for a,b being FinSequence of D st a in X &
b in X holds len a = len b
proof
assume X in A;
then
ex Y being set st Y = X & Y c= D* & for a,b being FinSequence of D
st a in Y & b in Y holds len a=len b by A2;
hence thesis;
end;
thus thesis by A2;
end;
hence thesis by Def7;
end;
end;
definition
let D be non empty set;
mode relation of D is Element of relations_on D;
end;
reserve a,b for FinSequence of D;
reserve p,r for Element of relations_on D;
theorem
X c= r implies X is Element of relations_on D
proof
assume
A1: X c= r;
then
A2: for a,b st a in X & b in X holds len a = len b by Def7;
r c= D* by Def7;
then X c= D* by A1;
hence thesis by A2,Def7;
end;
theorem
{a} is Element of relations_on D
proof
A1: for a1,a2 being FinSequence of D st a1 in {a} & a2 in {a} holds len a1 =
len a2
proof
let a1,a2 be FinSequence of D;
assume that
A2: a1 in {a} and
A3: a2 in {a};
a1 = a by A2,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
a in D* by FINSEQ_1:def 11;
then {a} c= D* by ZFMISC_1:31;
hence thesis by A1,Def7;
end;
theorem
for x,y being Element of D holds {<*x,y*>} is Element of relations_on D
proof
let x,y be Element of D;
A1: for a1,a2 being FinSequence of D st a1 in {<*x,y*>} & a2 in {<*x,y*>}
holds len a1 = len a2
proof
let a1,a2 be FinSequence of D;
assume that
A2: a1 in {<*x,y*>} and
A3: a2 in {<*x,y*>};
a1 = <*x,y*> by A2,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
<*x*>^<*y*> is FinSequence of D;
then <*x,y*> in D* by FINSEQ_1:def 11;
then {<*x,y*>} c= D* by ZFMISC_1:31;
hence thesis by A1,Def7;
end;
definition
let D,p,r;
redefine pred p = r means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for a holds a in p iff a in r;
compatibility
proof
thus p = r implies for a holds a in p iff a in r;
assume
A1: for a holds a in p iff a in r;
now
let x be object;
A2: now
assume
A3: x in r;
r is Subset of D* by Def7;
then x is FinSequence of D by A3,FINSEQ_1:def 11;
hence x in p by A1,A3;
end;
now
assume
A4: x in p;
p is Subset of D* by Def7;
then x is FinSequence of D by A4,FINSEQ_1:def 11;
hence x in r by A1,A4;
end;
hence x in p iff x in r by A2;
end;
hence thesis by TARSKI:2;
end;
end;
scheme
relDexist{D() -> non empty set, P[FinSequence of D()]}: ex r being Element
of relations_on D() st for a being FinSequence of D() holds a in r iff P[a]
provided
A1: for a,b being FinSequence of D() st P[a] & P[b] holds len a = len b
proof
defpred P1[object] means
ex a being FinSequence of D() st P[a] & $1 = a;
consider X being set such that
A2: for x being object holds x in X iff x in D()* & P1[x] from XBOOLE_0:sch 1;
A3: for a,b being FinSequence of D() st a in X & b in X holds len a = len b
proof
let a,b be FinSequence of D();
assume that
A4: a in X and
A5: b in X;
A6: ex d being FinSequence of D() st P[d] & b = d by A2,A5;
ex c being FinSequence of D() st P[c] & a = c by A2,A4;
hence thesis by A1,A6;
end;
for x being object holds x in X implies x in D()* by A2;
then X c= D()*;
then reconsider r = X as Element of relations_on D() by A3,Def7;
for a being FinSequence of D() holds a in r iff P[a]
proof
let a be FinSequence of D();
A7: now
A8: a in D()* by FINSEQ_1:def 11;
assume P[a];
hence a in r by A2,A8;
end;
now
assume a in r;
then ex c being FinSequence of D() st P[c] & a = c by A2;
hence P[a];
end;
hence thesis by A7;
end;
hence thesis;
end;
definition
let D;
func empty_rel(D) -> Element of relations_on D means
:Def9:
not a in it;
existence
proof
defpred P[FinSequence of D] means contradiction;
A1: P[a] & P[b] implies len a = len b;
consider r such that
A2: for a holds a in r iff P[a] from relDexist(A1);
take r;
thus thesis by A2;
end;
uniqueness;
end;
theorem
empty_rel(D) = {}
proof
assume
A1: not thesis;
set x = the Element of empty_rel(D);
empty_rel(D) is Subset of D* by Def7;
then x in D* by A1,TARSKI:def 3;
then reconsider a = x as FinSequence of D by FINSEQ_1:def 11;
a in empty_rel(D) by A1;
hence contradiction by Def9;
end;
definition
let D,p;
assume
A1: p <> empty_rel(D);
func the_arity_of p -> Element of NAT means
a in p implies it = len a;
existence
proof
consider c being FinSequence of D such that
A2: c in p by A1,Def9;
a in p implies len c = len a by A2,Def7;
hence thesis;
end;
uniqueness
proof
let n1,n2 be Element of NAT;
assume that
A3: a in p implies n1 = len a and
A4: a in p implies n2 = len a;
consider a such that
A5: a in p by A1,Def9;
len a = n1 by A3,A5;
hence thesis by A4,A5;
end;
end;
scheme
relDexist2{D() -> non empty set, k() -> Element of NAT, P[FinSequence of D()
]}: ex r being Element of relations_on D() st for a being FinSequence of D() st
len a = k() holds a in r iff P[a] proof
defpred P1[object] means
ex a being FinSequence of D() st len a = k() & P[a] & $1 = a;
consider X being set such that
A1: for x being object holds x in X iff x in D()* & P1[x] from XBOOLE_0:sch 1;
A2: for a,b being FinSequence of D() st a in X & b in X holds len a = len b
proof
let a,b be FinSequence of D();
assume that
A3: a in X and
A4: b in X;
A5: ex d being FinSequence of D() st len d = k() & P[d] & b = d by A1,A4;
ex c being FinSequence of D() st len c = k() & P[c] & a = c by A1,A3;
hence thesis by A5;
end;
for x being object holds x in X implies x in D()* by A1;
then X c= D()*;
then reconsider r = X as Element of relations_on D() by A2,Def7;
for a being FinSequence of D() st len a = k() holds a in r iff P[a]
proof
let a be FinSequence of D() such that
A6: len a = k();
A7: now
A8: a in D()* by FINSEQ_1:def 11;
assume P[a];
hence a in r by A1,A6,A8;
end;
now
assume a in r;
then
ex c being FinSequence of D() st len c = k() & P[c] & a = c by A1;
hence P[a];
end;
hence thesis by A7;
end;
hence thesis;
end;
definition
func BOOLEAN -> set equals
{0,1};
coherence;
end;
registration
cluster BOOLEAN -> non empty;
coherence;
end;
definition
redefine func FALSE -> Element of BOOLEAN; :: redefines FALSE (XBOOLEAN, definition)
coherence by TARSKI:def 2;
redefine func TRUE -> Element of BOOLEAN; :: redefines TRUE (XBOOLEAN, definition)
coherence by TARSKI:def 2;
end;
definition
let x be object;
redefine attr x is boolean means :: redefines boolean (XBOOLEAN, definition)
:Def12:
x in BOOLEAN;
compatibility by TARSKI:def 2;
end;
registration
cluster -> boolean for Element of BOOLEAN;
coherence;
end;
reserve u,v,w for boolean object;
definition
let v;
redefine func 'not' v equals :: redefines 'not' (XBOOLEAN, definition)
TRUE if v = FALSE otherwise FALSE;
compatibility
proof
let w;
thus v = FALSE implies (w = 'not' v iff w = TRUE);
assume v <> FALSE;
then v = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
consistency;
let w;
redefine func v '&' w equals :: redefines '&' (XBOOLEAN, definition)
TRUE if v = TRUE & w =TRUE otherwise FALSE;
compatibility
proof
let u be object;
thus v = TRUE & w =TRUE implies (u = v '&' w iff u = TRUE);
assume v <> TRUE or w <>TRUE;
then v = FALSE or w = FALSE by XBOOLEAN:def 3;
hence thesis;
end;
consistency;
end;
definition
let v be Element of BOOLEAN;
redefine func 'not' v -> Element of BOOLEAN; :: redefines 'not' (MARGREL1, redefinition) → 'not' (XBOOLEAN, definition)
correctness by Def12;
let w be Element of BOOLEAN;
redefine func v '&' w -> Element of BOOLEAN; :: redefines '&' (MARGREL1, redefinition) → '&' (XBOOLEAN, definition)
correctness by Def12;
end;
::$CT
theorem
(v = FALSE iff 'not' v = TRUE) & (v = TRUE iff 'not' v = FALSE);
theorem
(v '&' w = TRUE iff v = TRUE & w = TRUE) & (v '&' w = FALSE iff v =
FALSE or w = FALSE) by XBOOLEAN:101,140;
theorem
FALSE '&' v = FALSE;
theorem
TRUE '&' v = v;
theorem
v '&' v = FALSE implies v = FALSE;
theorem
v '&' (w '&' u) = (v '&' w) '&' u;
definition
let X;
func ALL(X) -> set equals
:Def15:
TRUE if not FALSE in X otherwise FALSE;
correctness;
end;
registration
let X;
cluster ALL X -> boolean;
correctness by Def15;
end;
definition
let X;
redefine func ALL X -> Element of BOOLEAN; :: redefines ALL (MARGREL1, definition)
correctness by Def12;
end;
theorem
(not FALSE in X iff ALL(X) = TRUE) & (FALSE in X iff ALL(X) = FALSE)
by Def15;
begin :: Addenda
:: from VALUAT_1, 2007.03.15, A.T.
definition
let f be Relation;
attr f is boolean-valued means
:Def16:
rng f c= BOOLEAN;
end;
registration
cluster boolean-valued for Function;
existence
proof
take {};
thus rng {} c= BOOLEAN;
end;
end;
registration
let f be boolean-valued Function, x be object;
cluster f.x -> boolean;
coherence
proof
per cases;
suppose
not x in dom f;
then f.x = FALSE by FUNCT_1:def 2;
hence f.x in BOOLEAN;
end;
suppose
A1: x in dom f;
A2: rng f c= BOOLEAN by Def16;
f.x in rng f by A1,FUNCT_1:def 3;
hence f.x in BOOLEAN by A2;
end;
end;
end;
definition
let p be boolean-valued Function;
func 'not' p -> boolean-valued Function means
:Def17:
dom it = dom p &
for x being object st x in dom p holds it.x = 'not'(p.x);
existence
proof
deffunc F(object) = 'not'(p.$1);
consider q being Function such that
A1: dom q = dom p and
A2: for x being object st x in dom p holds q.x = F(x) from FUNCT_1:sch 3;
q is boolean-valued
proof
let x be object;
assume x in rng q;
then consider y being object such that
A3: y in dom q and
A4: x = q.y by FUNCT_1:def 3;
x = 'not'(p.y) by A1,A2,A3,A4;
then x = FALSE or x = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
hence thesis by A1,A2;
end;
uniqueness
proof
let q1,q2 be boolean-valued Function such that
A5: dom q1 = dom p and
A6: for x being object st x in dom p holds q1.x = 'not'(p.x) and
A7: dom q2 = dom p and
A8: for x being object st x in dom p holds q2.x = 'not'(p.x);
for x being object st x in dom p holds q1.x = q2.x
proof
let x be object;
assume
A9: x in dom p;
then q1.x = 'not'(p.x) by A6;
hence thesis by A8,A9;
end;
hence thesis by A5,A7;
end;
involutiveness
proof
let q,p be boolean-valued Function;
assume that
A10: dom q = dom p and
A11: for x being object st x in dom p holds q.x = 'not'(p.x);
thus dom p = dom q by A10;
let x be object;
assume
A12: x in dom q;
thus p.x = 'not' 'not'(p.x) .= 'not'(q.x) by A10,A11,A12;
end;
let q be boolean-valued Function;
func p '&' q -> boolean-valued Function means
:Def18:
dom it = dom p /\ dom
q & for x being object st x in dom it holds it.x = (p.x) '&' (q.x);
existence
proof
deffunc F(object) = (p.$1) '&' (q.$1);
consider s being Function such that
A13: dom s = dom p /\ dom q and
A14: for x being object st x in dom p /\ dom q holds s.x = F(x) from
FUNCT_1:sch 3;
s is boolean-valued
proof
let x be object;
assume x in rng s;
then consider y being object such that
A15: y in dom s and
A16: x = s.y by FUNCT_1:def 3;
x = (p.y) '&' (q.y) by A13,A14,A15,A16;
then x = FALSE or x = TRUE by XBOOLEAN:def 3;
hence thesis;
end;
hence thesis by A13,A14;
end;
uniqueness
proof
let s1,s2 be boolean-valued Function such that
A17: dom s1 = dom p /\ dom q and
A18: for x being object st x in dom s1 holds s1.x = (p.x) '&' (q.x) and
A19: dom s2 = dom p /\ dom q and
A20: for x being object st x in dom s2 holds s2.x = (p.x) '&' (q.x);
for x being object st x in dom s1 holds s1.x = s2.x
proof
let x be object;
assume
A21: x in dom s1;
then s1.x = (p.x) '&' (q.x) by A18;
hence thesis by A17,A19,A20,A21;
end;
hence thesis by A17,A19;
end;
commutativity;
idempotence;
end;
registration
let A be set;
cluster -> boolean-valued for Function of A,BOOLEAN;
coherence
by RELAT_1:def 19;
end;
definition
let A be non empty set;
let p be Function of A,BOOLEAN;
redefine func 'not' p -> Function of A,BOOLEAN means :: redefines 'not' (MARGREL1, definition)
for x being Element of A holds it.x = 'not'(p.x);
coherence
proof
A1: dom 'not' p = dom p by Def17
.= A by PARTFUN1:def 2;
rng 'not' p c= BOOLEAN by Def16;
hence thesis by A1,FUNCT_2:2;
end;
compatibility
proof
let IT be Function of A,BOOLEAN;
A2: dom IT = A by FUNCT_2:def 1;
hereby
assume
A3: IT = 'not' p;
let x be Element of A;
x in A;
then x in dom p by FUNCT_2:def 1;
hence IT.x = 'not'(p.x) by A3,Def17;
end;
A4: dom p = A by FUNCT_2:def 1;
assume for x being Element of A holds IT.x = 'not'(p.x);
then for x being object st x in dom p holds IT.x = 'not'(p.x) by A4;
hence thesis by A2,A4,Def17;
end;
let q be Function of A,BOOLEAN;
redefine func p '&' q -> Function of A,BOOLEAN means :: redefines '&' (MARGREL1, definition)
for x being Element of A holds it.x = (p.x) '&' (q.x);
coherence
proof
A5: rng(p '&' q) c= BOOLEAN by Def16;
dom p = A & dom q = A by PARTFUN1:def 2;
then dom(p '&' q) = A /\ A by Def18
.= A;
hence thesis by A5,FUNCT_2:2;
end;
compatibility
proof
let IT be Function of A,BOOLEAN;
A6: dom IT = A by FUNCT_2:def 1;
hereby
assume
A7: IT = p '&' q;
let x be Element of A;
A8: dom q = A by FUNCT_2:def 1;
dom p = A by FUNCT_2:def 1;
then dom(p '&' q) = A /\ A by A8,Def18
.= A;
hence IT.x = (p.x) '&' (q.x) by A7,Def18;
end;
A9: dom q = A by FUNCT_2:def 1;
A10: dom IT = A /\ A by FUNCT_2:def 1
.= dom p /\ dom q by A9,FUNCT_2:def 1;
assume for x being Element of A holds IT.x = (p.x) '&' (q.x);
then for x being object st x in dom IT holds IT.x = (p.x) '&' (q.x) by A6;
hence thesis by A10,Def18;
end;
end;
begin :: Moved from UNIALG_1, 2010.03.16, A.T.
reserve A,z for set,
x,y for FinSequence of A,
h for PartFunc of A*,A,
n,m for Nat;
definition
let IT be Relation;
attr IT is homogeneous means
:Def21: dom IT is with_common_domain;
end;
definition
let A;
let IT be PartFunc of A*,A;
attr IT is quasi_total means
:Def22: for x,y st len x = len y & x in dom IT holds y in dom IT;
end;
registration
let f be Relation;
let X be with_common_domain set;
cluster f|X -> homogeneous;
coherence
proof
dom(f|X) c= X by RELAT_1:58;
hence dom(f|X) is with_common_domain;
end;
end;
registration
let A be non empty set, f be PartFunc of A*,A;
cluster dom f -> FinSequence-membered;
coherence
proof
dom f c= A* by RELAT_1:def 18;
hence thesis;
end;
end;
registration
let A be non empty set;
cluster homogeneous quasi_total non empty for PartFunc of A*,A;
existence
proof
set a = the Element of A;
set f = <*>A .-->a;
A2: dom f c= A*
proof
let z be object;
assume z in dom f;
then z = <*>A by TARSKI:def 1;
hence thesis by FINSEQ_1:def 11;
end;
A3: rng f = {a} by FUNCOP_1:8;
rng f c= A
proof
let z be object;
assume z in rng f;
then z = a by A3,TARSKI:def 1;
hence thesis;
end;
then reconsider f as PartFunc of A*,A by A2,RELSET_1:4;
A4: f is quasi_total
proof
let x,y be FinSequence of A;
assume that
A5: len x = len y and
A6: x in dom f;
x = <*>A by A6,TARSKI:def 1;
then len x = 0;
then y = <*>A by A5;
hence thesis by TARSKI:def 1;
end;
f is homogeneous;
hence thesis by A4;
end;
end;
registration
cluster homogeneous non empty for Function;
existence
proof
set f = the homogeneous non empty PartFunc of {{}}*,{{}};
take f;
thus thesis;
end;
end;
registration let R be homogeneous Relation;
cluster dom R -> with_common_domain;
coherence by Def21;
end;
theorem Th17:
for A being non empty set, a being Element of A holds <*>A .-->a
is homogeneous quasi_total non empty PartFunc of A*,A
proof
let A be non empty set, a be Element of A;
set f = <*>A .-->a;
A2: dom f c= A*
proof
let z be object;
assume z in dom f;
then z = <*>A by TARSKI:def 1;
hence thesis by FINSEQ_1:def 11;
end;
A3: rng f = {a} by FUNCOP_1:8;
rng f c= A
proof
let z be object;
assume z in rng f;
then z = a by A3,TARSKI:def 1;
hence thesis;
end;
then reconsider f as PartFunc of A*,A by A2,RELSET_1:4;
A4: f is quasi_total
proof
let x,y be FinSequence of A;
assume that
A5: len x = len y and
A6: x in dom f;
x = <*>A by A6,TARSKI:def 1;
then len x = 0;
then y = <*>A by A5;
hence thesis by TARSKI:def 1;
end;
f is homogeneous;
hence thesis by A4;
end;
theorem
for A being non empty set, a being Element of A holds <*>A .-->a
is Element of PFuncs(A*,A)
proof
let A be non empty set, a be Element of A;
set f = <*>A .-->a;
A2: dom f c= A*
proof
let z be object;
assume z in dom f;
then z = <*>A by TARSKI:def 1;
hence thesis by FINSEQ_1:def 11;
end;
A3: rng f = {a} by FUNCOP_1:8;
rng f c= A
proof
let z be object;
assume z in rng f;
then z = a by A3,TARSKI:def 1;
hence thesis;
end;
then reconsider f as PartFunc of A*,A by A2,RELSET_1:4;
f in PFuncs(A*,A) by PARTFUN1:45;
hence thesis;
end;
definition
let A;
mode PFuncFinSequence of A is FinSequence of PFuncs(A*,A);
end;
definition
let A;
let IT be PFuncFinSequence of A;
attr IT is homogeneous means
:Def23:
for n,h st n in dom IT & h = IT.n holds h is homogeneous;
end;
definition
let A;
let IT be PFuncFinSequence of A;
attr IT is quasi_total means
for n,h st n in dom IT & h = IT.n holds h is quasi_total;
end;
definition
let A be non empty set;
let x be Element of PFuncs(A*,A);
redefine func <*x*> -> PFuncFinSequence of A; :: redefines <* (FINSEQ_1, definition)
coherence
proof
<*x*> is FinSequence of PFuncs(A*,A);
hence thesis;
end;
end;
registration
let A be non empty set;
cluster homogeneous quasi_total non-empty for PFuncFinSequence of A;
existence
proof
set a = the Element of A;
reconsider f = <*>A .-->a as PartFunc of A*,A by Th17;
reconsider f as Element of PFuncs(A*,A) by PARTFUN1:45;
take <*f*>;
thus <*f*> is homogeneous
proof
let n;
let h be PartFunc of A*,A;
assume that
A1: n in dom <*f*> and
A2: h =<*f*>.n;
n in {1} by A1,FINSEQ_1:2,def 8;
then h = <*f*>.1 by A2,TARSKI:def 1;
then h = f;
hence thesis;
end;
thus <*f*> is quasi_total
proof
let n;
let h be PartFunc of A*,A;
assume that
A3: n in dom <*f*> and
A4: h =<*f*>.n;
n in {1} by A3,FINSEQ_1:2,def 8;
then h = <*f*>.1 by A4,TARSKI:def 1;
then h = f;
hence thesis by Th17;
end;
thus <*f*> is non-empty
proof
let n be object;
assume
A5: n in dom <*f*>;
then reconsider n as Element of NAT;
n in {1} by A5,FINSEQ_1:2,def 8;
then n = 1 by TARSKI:def 1;
hence thesis;
end;
end;
end;
registration
let A be non empty set;
let f be homogeneous PFuncFinSequence of A;
let i be set;
cluster f.i -> homogeneous;
coherence
proof
per cases;
suppose i in dom f;
hence thesis by Def23;
end;
suppose not i in dom f;
hence thesis by FUNCT_1:def 2,RELAT_1:38;
end;
end;
end;
reserve A for non empty set,
h for PartFunc of A*,A,
a for Element of A;
theorem
for x be Element of PFuncs(A*,A) st x = <*>A .--> a holds <*x*>
is homogeneous quasi_total non-empty
proof
let x be Element of PFuncs(A*,A) such that
A1: x = <*>A .--> a;
A2: for n,h st n in dom <*x*> & h = <*x*>.n holds h is homogeneous
proof
let n,h;
assume that
A3: n in dom <*x*> and
A4: h =<*x*>.n;
n in {1} by A3,FINSEQ_1:2,def 8;
then h = <*x*>.1 by A4,TARSKI:def 1;
then h = x;
hence thesis by A1;
end;
A5: for n,h st n in dom <*x*> & h = <*x*>.n holds h is quasi_total
proof
let n,h;
assume that
A6: n in dom <*x*> and
A7: h =<*x*>.n;
n in {1} by A6,FINSEQ_1:2,def 8;
then h = <*x*>.1 by A7,TARSKI:def 1;
then h = x;
hence thesis by A1,Th17;
end;
for n being object st n in dom <*x*> holds <*x*>.n is non empty
proof
let n be object;
assume n in dom <*x*>;
then n in {1} by FINSEQ_1:2,def 8;
then <*x*>.n = <*x*>.1 by TARSKI:def 1;
hence thesis by A1;
end;
hence thesis by A2,A5,FUNCT_1:def 9;
end;
definition
let f be homogeneous Relation;
func arity(f) -> Nat means
:Def25: for x being FinSequence st x in dom f holds it =
len x if ex x being FinSequence st x in dom f otherwise it = 0;
consistency;
existence
proof
thus (ex x being FinSequence st x in dom f) implies ex n st for x being
FinSequence st x in dom f holds n = len x
proof
given x being FinSequence such that
A1: x in dom f;
take len x;
let y be FinSequence;
assume y in dom f;
then dom x = dom y by A1,CARD_3:def 10;
hence thesis by FINSEQ_3:29;
end;
thus thesis;
end;
uniqueness
proof
let n,m;
hereby
given x0 being FinSequence such that
A2: x0 in dom f;
assume that
A3: for x being FinSequence st x in dom f holds n = len x and
A4: for x being FinSequence st x in dom f holds m = len x;
n = len x0 by A2,A3;
hence n = m by A2,A4;
end;
thus thesis;
end;
end;
definition
let f be homogeneous Function;
redefine func arity(f) -> Element of NAT; :: redefines arity (MARGREL1, definition)
coherence by ORDINAL1:def 12;
end;
begin :: Moved from UNIALG_2, 2010.03.17, A.T.
theorem
for n be Nat, D be non empty set, D1 be non empty Subset of D
holds n-tuples_on D /\ n-tuples_on D1 = n-tuples_on D1
proof
let n be Nat,D be non empty set, D1 be non empty Subset of D;
n-tuples_on D1 c= n-tuples_on D
proof
let z be object;
assume z in n-tuples_on D1;
then z is Tuple of n,D1 by FINSEQ_2:131;
then z is Element of n-tuples_on D by FINSEQ_2:109;
hence thesis;
end;
hence thesis by XBOOLE_1:28;
end;
theorem
for D being non empty set for h being homogeneous quasi_total non
empty PartFunc of D*,D holds dom h = (arity(h))-tuples_on D
proof
let D be non empty set;
let f be homogeneous quasi_total non empty PartFunc of D*,D;
set y = the Element of dom f;
A1: dom f c= D* by RELAT_1:def 18;
then
A2: y in D*;
thus dom f c= (arity(f))-tuples_on D
proof
let x be object;
assume
A3: x in dom f;
then reconsider x9 = x as FinSequence of D by A1,FINSEQ_1:def 11;
len x9 = arity f by A3,Def25;
then x9 is Element of (arity(f))-tuples_on D by FINSEQ_2:92;
hence thesis;
end;
reconsider y as FinSequence of D by A2,FINSEQ_1:def 11;
let x be object;
assume x in (arity(f))-tuples_on D;
then x in {s where s is Element of D* : len s = arity(f)} by FINSEQ_2:def 4;
then
A4: ex s being Element of D* st x = s & len s = arity(f);
len y = arity f by Def25;
hence thesis by A4,Def22;
end;
definition
let D be non empty set;
mode PFuncsDomHQN of D -> non empty set means
:Def26:
for x be Element of it
holds x is homogeneous quasi_total non empty PartFunc of D*,D;
existence
proof
set a = the Element of D;
reconsider A = {{<*>D} -->a} as non empty set;
take A;
let x be Element of A;
x= <*>D .-->a by TARSKI:def 1;
hence thesis by Th17;
end;
end;
definition
let D be non empty set, P be PFuncsDomHQN of D;
redefine mode Element of P -> homogeneous quasi_total non empty PartFunc of :: redefines Element (SUBSET_1, definition)
D*,D;
coherence by Def26;
end;