:: Boolean Posets, Posets under Inclusion and Products of Relational
:: Structures
:: by Adam Grabowski and Robert Milewski
::
:: Received September 20, 1996
:: Copyright (c) 1996-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 LATTICES, LATTICE3, SUBSET_1, STRUCT_0, EQREL_1, XBOOLE_0,
PBOOLE, XXREAL_0, REWRITE1, WELLORD2, RELAT_1, ZFMISC_1, RELAT_2,
ORDERS_2, TARSKI, SETFAM_1, CAT_1, YELLOW_0, WELLORD1, ORDINAL2,
PRE_TOPC, RCOMP_1, PRALG_1, FUNCT_1, FUNCOP_1, CARD_3, RLVECT_2, NEWTON,
FUNCT_2, SEQM_3, ORDERS_3, YELLOW_1, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1,
SETFAM_1, FUNCT_1, WELLORD2, ORDERS_1, CARD_3, PBOOLE, TOLER_1, PARTFUN1,
FUNCT_2, STRUCT_0, ORDERS_2, TOPS_2, LATTICES, ORDERS_3, LATTICE3,
PRE_TOPC, FUNCOP_1, PRALG_1, YELLOW_0;
constructors SETFAM_1, WELLORD2, TOLER_1, TOPS_2, LATTICE3, YELLOW_0, PRALG_1,
ORDERS_3, CARD_3, RELSET_1;
registrations SUBSET_1, RELSET_1, PARTFUN1, FUNCOP_1, STRUCT_0, LATTICES,
PRE_TOPC, ORDERS_2, LATTICE3, YELLOW_0;
requirements SUBSET, BOOLE;
definitions LATTICE3, XBOOLE_0, TOPS_2, TARSKI, RELAT_1, PRALG_1;
equalities LATTICE3, XBOOLE_0, RELAT_1;
expansions LATTICE3, XBOOLE_0, TOPS_2, TARSKI;
theorems TARSKI, LATTICES, LATTICE3, YELLOW_0, STRUCT_0, RELAT_1, ORDERS_2,
RELSET_1, ZFMISC_1, WELLORD2, SETFAM_1, PRE_TOPC, FUNCT_1, FUNCOP_1,
PBOOLE, CARD_3, FUNCT_2, PRALG_1, ORDERS_3, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes RELSET_1, FUNCT_2;
begin :: Boolean Posets and Posets under Inclusion
reserve X for set;
registration
let L be Lattice;
cluster LattPOSet L -> with_suprema with_infima;
coherence by LATTICE3:11;
end;
registration
let L be upper-bounded Lattice;
cluster LattPOSet L -> upper-bounded;
coherence
proof
ex x being Element of LattPOSet L st x is_>=_than the carrier of
LattPOSet L
proof
take x = Top (LattPOSet L);
consider z be Element of L such that
A1: for v being Element of L holds z"\/"v = z & v"\/"z = z by LATTICES:def 14
;
reconsider z9 = z as Element of LattPOSet L;
A2: z = Top L by A1,LATTICES:def 17;
A3: now
let b9 be Element of LattPOSet L;
reconsider b = b9 as Element of L;
assume b9 is_<=_than {};
A4: b% = b & z% = z;
b [= z by A2,LATTICES:19;
hence z9 >= b9 by A4,LATTICE3:7;
end;
z9 is_<=_than {};
then
A5: z9 = "/\"({},LattPOSet L) by A3,YELLOW_0:31;
now
reconsider x9 = x as Element of L;
let a be Element of LattPOSet L;
assume a in the carrier of LattPOSet L;
reconsider a9 = a as Element of L;
Top (LattPOSet L) = Top L by A2,A5,YELLOW_0:def 12;
then
A6: a9 [= x9 by LATTICES:19;
a9% = a9 & x9% = x9;
hence a <= x by A6,LATTICE3:7;
end;
hence thesis;
end;
hence thesis by YELLOW_0:def 5;
end;
end;
registration
let L be lower-bounded Lattice;
cluster LattPOSet L -> lower-bounded;
coherence
proof
ex x being Element of LattPOSet L st x is_<=_than the carrier of
LattPOSet L
proof
take x = Bottom (LattPOSet L);
consider z be Element of L such that
A1: for v being Element of L holds z"/\"v = z & v"/\"z = z by LATTICES:def 13
;
reconsider z9 = z as Element of LattPOSet L;
A2: z = Bottom L by A1,LATTICES:def 16;
A3: now
let b9 be Element of LattPOSet L;
reconsider b = b9 as Element of L;
assume b9 is_>=_than {};
A4: b% = b & z% = z;
z [= b by A2,LATTICES:16;
hence z9 <= b9 by A4,LATTICE3:7;
end;
z9 is_>=_than {};
then
A5: z9 = "\/"({},LattPOSet L) by A3,YELLOW_0:30;
now
reconsider x9 = x as Element of L;
let a be Element of LattPOSet L;
assume a in the carrier of LattPOSet L;
reconsider a9 = a as Element of L;
Bottom (LattPOSet L) = Bottom L by A2,A5,YELLOW_0:def 11;
then
A6: x9 [= a9 by LATTICES:16;
a9% = a9 & x9% = x9;
hence x <= a by A6,LATTICE3:7;
end;
hence thesis;
end;
hence thesis by YELLOW_0:def 4;
end;
end;
registration
let L be complete Lattice;
cluster LattPOSet L -> complete;
coherence
proof
for X be set ex a be Element of LattPOSet L st X is_<=_than a & for b
being Element of LattPOSet L st X is_<=_than b holds a <= b
proof
let X be set;
take a = "\/"(X,LattPOSet L);
X is_less_than "\/"(X,L) by LATTICE3:def 21;
then X is_<=_than "\/"(X,L)% by LATTICE3:30;
hence X is_<=_than a by YELLOW_0:29;
let b be Element of LattPOSet L;
reconsider b9 = b as Element of L;
assume X is_<=_than b;
then X is_<=_than b9%;
then X is_less_than b9 by LATTICE3:30;
then
A1: "\/"(X,L) [= b9 by LATTICE3:def 21;
"\/"(X,L)% = a & b9% = b by YELLOW_0:29;
hence thesis by A1,LATTICE3:7;
end;
hence thesis;
end;
end;
definition
let X be set;
func InclPoset X -> strict RelStr equals
RelStr(#X, RelIncl X#);
correctness;
end;
registration
let X be set;
cluster InclPoset X -> reflexive antisymmetric transitive;
coherence;
end;
registration
let X be non empty set;
cluster InclPoset X -> non empty;
coherence;
end;
theorem
the carrier of InclPoset X = X & the InternalRel of InclPoset X = RelIncl X;
definition
let X be set;
func BoolePoset X -> strict RelStr equals
LattPOSet BooleLatt X;
correctness;
end;
registration
let X be set;
cluster BoolePoset X -> non empty reflexive antisymmetric transitive;
coherence;
end;
registration
let X be set;
cluster BoolePoset X -> complete;
coherence;
end;
theorem Th2:
for x,y be Element of BoolePoset X holds x <= y iff x c= y
proof
let x,y be Element of BoolePoset X;
reconsider x9 = x, y9 = y as Element of BooleLatt X;
thus x <= y implies x c= y
proof
assume x <= y;
then x9% <= y9%;
then x9 [= y9 by LATTICE3:7;
hence thesis by LATTICE3:2;
end;
assume x c= y;
then x9 [= y9 by LATTICE3:2;
then x9% <= y9% by LATTICE3:7;
hence thesis;
end;
theorem Th3:
for X be non empty set, x,y be Element of InclPoset X holds x <= y iff x c= y
proof
let X be non empty set;
let x,y be Element of InclPoset X;
thus x <= y implies x c= y
proof
assume x <= y;
then [x,y] in the InternalRel of InclPoset X by ORDERS_2:def 5;
hence thesis by WELLORD2:def 1;
end;
thus x c= y implies x <= y
proof
assume x c= y;
then [x,y] in RelIncl X by WELLORD2:def 1;
hence thesis by ORDERS_2:def 5;
end;
end;
theorem Th4:
BoolePoset X = InclPoset bool X
proof
set B = BoolePoset X;
the carrier of B = bool X by LATTICE3:def 1;
then reconsider In = the InternalRel of B as Relation of bool X;
for x be object st x in bool X ex y be object st [x,y] in In
proof
let x be object;
assume x in bool X;
then reconsider x9 = x as Element of B by LATTICE3:def 1;
take y = x9;
x9 <= y;
hence thesis by ORDERS_2:def 5;
end;
then
A1: dom In = bool X by RELSET_1:9;
A2: now
let Y,Z be set;
assume Y in bool X & Z in bool X;
then reconsider Y9 = Y, Z9 = Z as Element of B by LATTICE3:def 1;
thus [Y,Z] in the InternalRel of B implies Y c= Z
proof
assume [Y,Z] in the InternalRel of B;
then Y9 <= Z9 by ORDERS_2:def 5;
hence thesis by Th2;
end;
thus Y c= Z implies [Y,Z] in the InternalRel of B
proof
assume Y c= Z;
then Y9 <= Z9 by Th2;
hence thesis by ORDERS_2:def 5;
end;
end;
for y be object st y in bool X ex x be object st [x,y] in In
proof
let y be object;
assume y in bool X;
then reconsider y9 = y as Element of B by LATTICE3:def 1;
take x = y9;
x <= y9;
hence thesis by ORDERS_2:def 5;
end;
then field the InternalRel of B = bool X \/ bool X by A1,RELSET_1:10;
then the InternalRel of B = RelIncl bool X by A2,WELLORD2:def 1;
hence thesis by LATTICE3:def 1;
end;
theorem
for Y be Subset-Family of X holds InclPoset Y is full SubRelStr of
BoolePoset X
proof
set L = BoolePoset X;
let Y be Subset-Family of X;
reconsider Y9 = Y as Subset of L by LATTICE3:def 1;
the carrier of L = bool X by LATTICE3:def 1;
then reconsider In = the InternalRel of L as Relation of bool X;
for x be object st x in bool X ex y be object st [x,y] in In
proof
let x be object;
assume x in bool X;
then reconsider x9 = x as Element of L by LATTICE3:def 1;
take y = x9;
x9 <= y;
hence thesis by ORDERS_2:def 5;
end;
then
A1: dom In = bool X by RELSET_1:9;
A2: now
let Y,Z be set;
assume Y in bool X & Z in bool X;
then reconsider Y9 = Y, Z9 = Z as Element of L by LATTICE3:def 1;
thus [Y,Z] in the InternalRel of L implies Y c= Z
proof
assume [Y,Z] in the InternalRel of L;
then Y9 <= Z9 by ORDERS_2:def 5;
hence thesis by Th2;
end;
thus Y c= Z implies [Y,Z] in the InternalRel of L
proof
assume Y c= Z;
then Y9 <= Z9 by Th2;
hence thesis by ORDERS_2:def 5;
end;
end;
for y be object st y in bool X ex x be object st [x,y] in In
proof
let y be object;
assume y in bool X;
then reconsider y9 = y as Element of L by LATTICE3:def 1;
take x = y9;
x <= y9;
hence thesis by ORDERS_2:def 5;
end;
then field the InternalRel of L = bool X \/ bool X by A1,RELSET_1:10;
then
A3: the InternalRel of L = RelIncl bool X by A2,WELLORD2:def 1;
RelStr(#Y9,(the InternalRel of L) |_2 Y9#) is full SubRelStr of L by
YELLOW_0:56;
hence thesis by A3,WELLORD2:7;
end;
theorem
for X be non empty set holds InclPoset X is with_suprema implies for x
,y be Element of InclPoset X holds x \/ y c= x "\/" y
proof
let X be non empty set;
assume
A1: InclPoset X is with_suprema;
let x,y be Element of InclPoset X;
y <= x "\/" y by A1,YELLOW_0:22;
then
A2: y c= x "\/" y by Th3;
x <= x "\/" y by A1,YELLOW_0:22;
then x c= x "\/" y by Th3;
hence thesis by A2,XBOOLE_1:8;
end;
theorem
for X be non empty set holds InclPoset X is with_infima implies for x,
y be Element of InclPoset X holds x "/\" y c= x /\ y
proof
let X be non empty set;
assume
A1: InclPoset X is with_infima;
let x,y be Element of InclPoset X;
x "/\" y <= y by A1,YELLOW_0:23;
then
A2: x "/\" y c= y by Th3;
x "/\" y <= x by A1,YELLOW_0:23;
then x "/\" y c= x by Th3;
hence thesis by A2,XBOOLE_1:19;
end;
theorem Th8:
for X be non empty set holds for x,y be Element of InclPoset X st
x \/ y in X holds x "\/" y = x \/ y
proof
let X be non empty set;
let x,y be Element of InclPoset X;
assume x \/ y in X;
then reconsider z = x \/ y as Element of InclPoset X;
y c= z by XBOOLE_1:7;
then
A1: y <= z by Th3;
A2: now
let c be Element of InclPoset X;
assume x <= c & y <= c;
then x c= c & y c= c by Th3;
then z c= c by XBOOLE_1:8;
hence z <= c by Th3;
end;
x c= z by XBOOLE_1:7;
then x <= z by Th3;
hence thesis by A1,A2,LATTICE3:def 13;
end;
theorem Th9:
for X be non empty set for x,y be Element of InclPoset X st x /\
y in X holds x "/\" y = x /\ y
proof
let X be non empty set;
let x,y be Element of InclPoset X;
assume x /\ y in X;
then reconsider z = x /\ y as Element of InclPoset X;
z c= y by XBOOLE_1:17;
then
A1: z <= y by Th3;
A2: now
let c be Element of InclPoset X;
assume c <= x & c <= y;
then c c= x & c c= y by Th3;
then c c= z by XBOOLE_1:19;
hence c <= z by Th3;
end;
z c= x by XBOOLE_1:17;
then z <= x by Th3;
hence thesis by A1,A2,LATTICE3:def 14;
end;
theorem
for L be RelStr st for x,y be Element of L holds x <= y iff x c= y
holds the InternalRel of L = RelIncl the carrier of L
proof
let L be RelStr;
assume
A1: for x,y be Element of L holds x <= y iff x c= y;
A2: now
let Y,Z be set;
assume Y in the carrier of L & Z in the carrier of L;
then reconsider Y9 = Y, Z9 = Z as Element of L;
thus [Y,Z] in the InternalRel of L implies Y c= Z
proof
assume [Y,Z] in the InternalRel of L;
then Y9 <= Z9 by ORDERS_2:def 5;
hence thesis by A1;
end;
thus Y c= Z implies [Y,Z] in the InternalRel of L
proof
assume Y c= Z;
then Y9 <= Z9 by A1;
hence thesis by ORDERS_2:def 5;
end;
end;
for x be object st x in the carrier of L ex y be object st [x,y] in the
InternalRel of L
proof
let x be object;
assume x in the carrier of L;
then reconsider x9 = x as Element of L;
take y = x9;
x9 <= y by A1;
hence thesis by ORDERS_2:def 5;
end;
then
A3: dom the InternalRel of L = the carrier of L by RELSET_1:9;
for y be object st y in the carrier of L
ex x be object st [x,y] in the InternalRel of L
proof
let y be object;
assume y in the carrier of L;
then reconsider y9 = y as Element of L;
take x = y9;
x <= y9 by A1;
hence thesis by ORDERS_2:def 5;
end;
then field the InternalRel of L = (the carrier of L) \/ the carrier of L by
A3,RELSET_1:10;
hence thesis by A2,WELLORD2:def 1;
end;
theorem
for X be non empty set st (for x,y be set st (x in X & y in X) holds x
\/ y in X) holds InclPoset X is with_suprema
proof
let X be non empty set;
set L = InclPoset X;
assume
A1: for x,y be set st x in X & y in X holds x \/ y in X;
now
let a,b be Element of L;
ex c be Element of L st {a,b} is_<=_than c & for d be Element of L st
{a,b} is_<=_than d holds c <= d
proof
take c = a "\/" b;
A2: a \/ b = c by A1,Th8;
then b c= c by XBOOLE_1:7;
then
A3: b <= c by Th3;
a c= c by A2,XBOOLE_1:7;
then a <= c by Th3;
hence {a,b} is_<=_than c by A3,YELLOW_0:8;
let d be Element of L;
assume
A4: {a,b} is_<=_than d;
b in {a,b} by TARSKI:def 2;
then b <= d by A4;
then
A5: b c= d by Th3;
a in {a,b} by TARSKI:def 2;
then a <= d by A4;
then a c= d by Th3;
then a \/ b c= d by A5,XBOOLE_1:8;
then c c= d by A1,Th8;
hence thesis by Th3;
end;
hence ex_sup_of {a,b}, L by YELLOW_0:15;
end;
hence thesis by YELLOW_0:20;
end;
theorem
for X be non empty set st for x,y be set st x in X & y in X holds x /\
y in X holds InclPoset X is with_infima
proof
let X be non empty set;
set L = InclPoset X;
assume
A1: for x,y be set st x in X & y in X holds x /\ y in X;
now
let a,b be Element of L;
ex c be Element of L st {a,b} is_>=_than c & for d be Element of L st
{a,b} is_>=_than d holds c >= d
proof
take c = a "/\" b;
A2: a /\ b = c by A1,Th9;
then c c= b by XBOOLE_1:17;
then
A3: c <= b by Th3;
c c= a by A2,XBOOLE_1:17;
then c <= a by Th3;
hence {a,b} is_>=_than c by A3,YELLOW_0:8;
let d be Element of L;
assume
A4: {a,b} is_>=_than d;
b in {a,b} by TARSKI:def 2;
then d <= b by A4;
then
A5: d c= b by Th3;
a in {a,b} by TARSKI:def 2;
then d <= a by A4;
then d c= a by Th3;
then d c= a /\ b by A5,XBOOLE_1:19;
then d c= c by A1,Th9;
hence thesis by Th3;
end;
hence ex_inf_of {a,b},L by YELLOW_0:16;
end;
hence thesis by YELLOW_0:21;
end;
theorem Th13:
for X be non empty set holds {} in X implies Bottom InclPoset X = {}
proof
let X be non empty set;
assume {} in X;
then reconsider a = {} as Element of InclPoset X;
for b be Element of InclPoset X st b in X holds a <= b by Th3,XBOOLE_1:2;
then a is_<=_than X;
then InclPoset X is lower-bounded by YELLOW_0:def 4;
then {} is_<=_than a & ex_sup_of {},InclPoset X by YELLOW_0:42;
then "\/"({},InclPoset X) <= a by YELLOW_0:def 9;
then
A1: "\/"({},InclPoset X) c= a by Th3;
thus Bottom InclPoset X = "\/"({},InclPoset X) by YELLOW_0:def 11
.= {} by A1;
end;
theorem Th14:
for X be non empty set holds union X in X implies Top InclPoset X = union X
proof
let X be non empty set;
assume union X in X;
then reconsider a = union X as Element of InclPoset X;
for b be Element of InclPoset X st b in X holds b <= a by Th3,ZFMISC_1:74;
then a is_>=_than X;
then InclPoset X is upper-bounded by YELLOW_0:def 5;
then {} is_>=_than a & ex_inf_of {},InclPoset X by YELLOW_0:43;
then a <= "/\"({},InclPoset X) by YELLOW_0:def 10;
then
A1: "/\"({},InclPoset X) c= a & a c= "/\"({},InclPoset X) by Th3,ZFMISC_1:74;
thus Top InclPoset X = "/\"({},InclPoset X) by YELLOW_0:def 12
.= union X by A1;
end;
theorem
for X being non empty set holds InclPoset X is upper-bounded implies
union X in X
proof
let X be non empty set;
assume InclPoset X is upper-bounded;
then consider x be Element of InclPoset X such that
A1: x is_>=_than the carrier of InclPoset X by YELLOW_0:def 5;
now
let y be object;
assume y in union X;
then consider Y be set such that
A2: y in Y and
A3: Y in X by TARSKI:def 4;
reconsider Y as Element of InclPoset X by A3;
Y <= x by A1;
then Y c= x by Th3;
hence y in x by A2;
end;
then
A4: union X c= x;
x in X & x c= union X by ZFMISC_1:74;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem
for X be non empty set holds InclPoset X is lower-bounded implies meet X in X
proof
let X be non empty set;
assume InclPoset X is lower-bounded;
then consider x be Element of InclPoset X such that
A1: x is_<=_than the carrier of InclPoset X by YELLOW_0:def 4;
now
let y be object;
assume
A2: y in x;
now
let Y be set;
assume Y in X;
then reconsider Y9 = Y as Element of InclPoset X;
x <= Y9 by A1;
then x c= Y9 by Th3;
hence y in Y by A2;
end;
hence y in meet X by SETFAM_1:def 1;
end;
then
A3: x c= meet X;
x in X & meet X c= x by SETFAM_1:3;
hence thesis by A3,XBOOLE_0:def 10;
end;
Lm1: for x,y be Element of BoolePoset X holds x /\ y in bool X & x \/ y in
bool X
proof
let x,y be Element of BoolePoset X;
x in the carrier of BoolePoset X;
then
A1: x in bool X by LATTICE3:def 1;
then x /\ y c= X by XBOOLE_1:108;
hence x /\ y in bool X;
y in the carrier of BoolePoset X;
then y in bool X by LATTICE3:def 1;
then x \/ y c= X by A1,XBOOLE_1:8;
hence thesis;
end;
theorem
for x,y be Element of BoolePoset X holds x "\/" y = x \/ y & x "/\" y
= x /\ y
proof
let x,y be Element of BoolePoset X;
reconsider x, y as Element of InclPoset bool X by Th4;
x "/\" y = x /\ y & x "\/" y = x \/ y by Lm1,Th8,Th9;
hence thesis by Th4;
end;
theorem
Bottom BoolePoset X = {}
proof
thus Bottom BoolePoset X = "\/"({},LattPOSet BooleLatt X) by YELLOW_0:def 11
.= "\/"({},BooleLatt X) by YELLOW_0:29
.= Bottom BooleLatt X by LATTICE3:49
.= {} by LATTICE3:3;
end;
theorem
Top BoolePoset X = X
proof
A1: Top InclPoset bool X = union bool X by Th14;
BoolePoset X = InclPoset bool X by Th4;
hence thesis by A1,ZFMISC_1:81;
end;
theorem
for Y being non empty Subset of BoolePoset X holds inf Y = meet Y
proof
set L = BoolePoset X;
let Y be non empty Subset of L;
set y = the Element of Y;
A1: the carrier of L = bool X by LATTICE3:def 1;
then y c= X;
then reconsider Me = meet Y as Element of L by A1,SETFAM_1:7;
A2: now
let b be Element of L;
assume
A3: b is_<=_than Y;
for Z being set st Z in Y holds b c= Z by Th2,A3;
then b c= Me by SETFAM_1:5;
hence Me >= b by Th2;
end;
for b being Element of L st b in Y holds Me <= b by Th2,SETFAM_1:3;
then Me is_<=_than Y;
hence thesis by A2,YELLOW_0:33;
end;
theorem
for Y being Subset of BoolePoset X holds sup Y = union Y
proof
set L = BoolePoset X;
let Y be Subset of L;
A1: the carrier of L = bool X by LATTICE3:def 1;
then union Y c= union bool X by ZFMISC_1:77;
then reconsider Un = union Y as Element of L by A1,ZFMISC_1:81;
A2: now
let b be Element of L;
assume
A3: b is_>=_than Y;
for Z being set st Z in Y holds Z c= b by Th2,A3;
then Un c= b by ZFMISC_1:76;
hence Un <= b by Th2;
end;
for b being Element of L st b in Y holds b <= Un by Th2,ZFMISC_1:74;
then Un is_>=_than Y;
hence thesis by A2,YELLOW_0:30;
end;
theorem
for T being non empty TopSpace, X being Subset of InclPoset the
topology of T holds sup X = union X
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T;
let X be Subset of L;
reconsider X as Subset-Family of T by XBOOLE_1:1;
reconsider Un = union X as Element of L by PRE_TOPC:def 1;
A1: now
let b be Element of L;
assume b is_>=_than X;
then for Z being set st Z in X holds Z c= b by Th3;
then Un c= b by ZFMISC_1:76;
hence Un <= b by Th3;
end;
for b being Element of L st b in X holds b <= Un by Th3,ZFMISC_1:74;
then Un is_>=_than X;
hence thesis by A1,YELLOW_0:30;
end;
theorem
for T be non empty TopSpace holds Bottom InclPoset the topology of T =
{} by Th13,PRE_TOPC:1;
Lm2: for T be non empty TopSpace holds InclPoset the topology of T is
lower-bounded
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T;
reconsider x = {} as Element of L by PRE_TOPC:1;
now
take x;
thus x is_<=_than the carrier of L
proof
let b be Element of L;
assume b in the carrier of L;
x c= b;
hence thesis by Th3;
end;
end;
hence thesis by YELLOW_0:def 4;
end;
theorem
for T be non empty TopSpace holds Top InclPoset the topology of T =
the carrier of T
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T, C = the carrier of T;
the carrier of T = "/\"({},L)
proof
reconsider C as Element of L by PRE_TOPC:def 1;
A1: for b being Element of L st b is_<=_than {} holds C >= b
proof
let b be Element of L;
assume b is_<=_than {};
b in the topology of T;
hence thesis by Th3;
end;
C is_<=_than {};
hence thesis by A1,YELLOW_0:31;
end;
hence thesis by YELLOW_0:def 12;
end;
Lm3: for T being non empty TopSpace holds InclPoset the topology of T is
complete
proof
let T be non empty TopSpace;
set A = the topology of T;
reconsider IA = InclPoset A as lower-bounded Poset by Lm2;
for X be Subset of IA holds ex_sup_of X, InclPoset A
proof
let X be Subset of IA;
set N = union X;
reconsider X9 = X as Subset-Family of T by XBOOLE_1:1;
X9 c= the topology of T;
then reconsider N as Element of InclPoset A by PRE_TOPC:def 1;
A1: for b being Element of InclPoset A st X is_<=_than b holds N <= b
proof
let b be Element of InclPoset A;
assume X is_<=_than b;
then for Z1 being set st Z1 in X holds Z1 c= b by Th3;
then union X c= b by ZFMISC_1:76;
hence thesis by Th3;
end;
X is_<=_than N
by ZFMISC_1:74,Th3;
hence thesis by A1,YELLOW_0:15;
end;
hence thesis by YELLOW_0:53;
end;
Lm4: for T being non empty TopSpace holds InclPoset the topology of T is non
trivial
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T;
reconsider E = {}, S = the carrier of T as Element of L by PRE_TOPC:1,def 1;
E <> S;
hence thesis by STRUCT_0:def 10;
end;
registration
let T be non empty TopSpace;
cluster InclPoset the topology of T -> complete non trivial;
coherence by Lm3,Lm4;
end;
theorem
for T being TopSpace, F being Subset-Family of T holds F is open iff F
is Subset of InclPoset the topology of T
proof
let T be TopSpace;
let F be Subset-Family of T;
hereby
assume
A1: F is open;
F c= the topology of T
by A1,PRE_TOPC:def 2;
hence F is Subset of InclPoset the topology of T;
end;
assume
A2: F is Subset of InclPoset the topology of T;
let P be Subset of T;
assume P in F;
hence thesis by A2,PRE_TOPC:def 2;
end;
begin :: Products of Relational Structures
reserve x,y,z for set;
definition
let R be Relation;
attr R is RelStr-yielding means
:Def3:
for v being set st v in rng R holds v is RelStr;
end;
registration
cluster RelStr-yielding -> 1-sorted-yielding for Function;
coherence
proof
let F be Function such that
A1: F is RelStr-yielding;
let x be object;
assume x in dom F;
then F.x in rng F by FUNCT_1:def 3;
hence thesis by A1;
end;
end;
registration
let I be set;
cluster RelStr-yielding for ManySortedSet of I;
existence
proof
set R = the RelStr;
take I --> R;
let v be set;
assume
A1: v in rng(I-->R);
rng(I-->R) c= {R} by FUNCOP_1:13;
hence thesis by A1,TARSKI:def 1;
end;
end;
definition
let J be non empty set, A be RelStr-yielding ManySortedSet of J, j be
Element of J;
redefine func A.j -> RelStr; :: redefines . (FUNCT_1, definition)
coherence
proof
dom A = J by PARTFUN1:def 2;
then A.j in rng A by FUNCT_1:def 3;
hence thesis by Def3;
end;
end;
definition
let I be set;
let J be RelStr-yielding ManySortedSet of I;
func product J -> strict RelStr means
:Def4:
the carrier of it = product
Carrier J & for x,y being Element of it st x in product Carrier J holds x <= y
iff ex f,g being Function st f = x & g = y &
for i be object st i in I ex R being
RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi;
existence
proof
defpred P[object,object] means
ex f,g being Function st f = $1 & g = $2 &
for i be object st i in I
ex R being RelStr, xi,yi being Element of R st R = J.i & xi =
f.i & yi = g.i & xi <= yi;
consider R being Relation of product Carrier J such that
A1: for x,y being object holds [x,y] in R iff x in product Carrier J & y
in product Carrier J & P[x, y] from RELSET_1:sch 1;
take RS = RelStr(#product Carrier J,R#);
thus the carrier of RS = product Carrier J;
let x,y be Element of RS such that
A2: x in product Carrier J;
hereby
assume x <= y;
then [x,y] in the InternalRel of RS by ORDERS_2:def 5;
hence ex f,g being Function st f = x & g = y &
for i be object st i in I ex
R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi
<= yi by A1;
end;
assume ex f,g being Function st f = x & g = y &
for i be object st i in I ex
R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi
<= yi;
then [x,y] in the InternalRel of RS by A1,A2;
hence thesis by ORDERS_2:def 5;
end;
uniqueness
proof
let S1,S2 be strict RelStr such that
A3: the carrier of S1 = product Carrier J and
A4: for x,y being Element of S1 st x in product Carrier J holds x <= y
iff ex f,g being Function st f = x & g = y &
for i be object st i in I ex R being
RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <= yi
and
A5: the carrier of S2 = product Carrier J and
A6: for x,y being Element of S2 st x in product Carrier J holds x <=
y iff ex f,g being Function st f = x & g = y &
for i be object st i in I ex R
being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi <=
yi;
the InternalRel of S1 = the InternalRel of S2
proof
let a,b be object;
hereby
assume
A7: [a,b] in the InternalRel of S1;
then reconsider x=a, y=b as Element of S1 by ZFMISC_1:87;
reconsider x9=x, y9=y as Element of S2 by A3,A5;
A8: a in the carrier of S1 by A7,ZFMISC_1:87;
x <= y by A7,ORDERS_2:def 5;
then ex f,g being Function st f = x & g = y &
for i be object st i in I
ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i &
xi <= yi by A3,A4,A8;
then x9 <= y9 by A3,A6,A8;
hence [a,b] in the InternalRel of S2 by ORDERS_2:def 5;
end;
assume
A9: [a,b] in the InternalRel of S2;
then reconsider x=a, y=b as Element of S2 by ZFMISC_1:87;
reconsider x9=x, y9=y as Element of S1 by A3,A5;
A10: a in the carrier of S2 by A9,ZFMISC_1:87;
x <= y by A9,ORDERS_2:def 5;
then ex f,g being Function st f = x & g = y &
for i be object st i in I ex
R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i & yi = g.i & xi
<= yi by A5,A6,A10;
then x9 <= y9 by A4,A5,A10;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by A3,A5;
end;
end;
registration
let X be set;
let L be RelStr;
cluster X --> L -> RelStr-yielding;
coherence
proof
let v be set;
assume
A1: v in rng(X-->L);
rng(X-->L) c= {L} by FUNCOP_1:13;
hence thesis by A1,TARSKI:def 1;
end;
end;
definition
let I be set;
let T be RelStr;
func T|^I -> strict RelStr equals
product (I --> T);
correctness;
end;
theorem Th26:
for J be RelStr-yielding ManySortedSet of {} holds product J =
RelStr (#{{}}, id {{}}#)
proof
let J be RelStr-yielding ManySortedSet of {};
set IT = product J;
A1: the carrier of IT = product Carrier J by Def4
.= {{}} by CARD_3:10,PBOOLE:122;
A2: product Carrier J = {{}} by CARD_3:10,PBOOLE:122;
the InternalRel of product J = id {{}}
proof
reconsider x = {}, y = {} as Element of IT by A1,TARSKI:def 1;
let a,b be object;
x = {} --> {{}};
then reconsider f = x, g = y as Function;
hereby
assume
A3: [a,b] in the InternalRel of IT;
then
A4: b in the carrier of IT by ZFMISC_1:87;
A5: a in the carrier of IT by A3,ZFMISC_1:87;
then a = {} by A1,TARSKI:def 1;
then a = b by A1,A4,TARSKI:def 1;
hence [a,b] in id {{}} by A1,A5,RELAT_1:def 10;
end;
assume
A6: [a,b] in id {{}};
then a in {{}} by RELAT_1:def 10;
then
A7: a = {} by TARSKI:def 1;
for i be object st i in {} ex R being RelStr, xi,yi being Element of R
st R = J.i & xi = f.i & yi = g.i & xi <= yi;
then
A8: x <= y by A1,A2,Def4;
a = b by A6,RELAT_1:def 10;
hence thesis by A7,A8,ORDERS_2:def 5;
end;
hence thesis by A1;
end;
theorem
for Y be RelStr holds Y|^{} = RelStr (#{{}}, id {{}}#) by Th26;
theorem Th28:
for X be set, Y be RelStr holds Funcs (X, the carrier of Y) =
the carrier of Y|^X
proof
let X be set;
let Y be RelStr;
set YY = the carrier of Y, f = Carrier (X --> Y);
A1: dom f = X by PARTFUN1:def 2;
A2: for x be set st x in X holds f.x = YY
proof
let x be set;
assume
A3: x in X;
then ex R being 1-sorted st R = (X --> Y).x & f.x = the carrier of R by
PRALG_1:def 15;
hence thesis by A3,FUNCOP_1:7;
end;
Funcs(X,YY) = product f
proof
thus Funcs(X,YY) c= product f
proof
let x be object;
assume x in Funcs(X,YY);
then consider g be Function such that
A4: x = g and
A5: dom g = X and
A6: rng g c= YY by FUNCT_2:def 2;
now
let y be object;
assume y in dom f;
then f.y = YY & g.y in rng g by A2,A5,FUNCT_1:def 3;
hence g.y in f.y by A6;
end;
hence thesis by A1,A4,A5,CARD_3:def 5;
end;
let x be object;
assume x in product f;
then consider g be Function such that
A7: x = g and
A8: dom g = dom f and
A9: for x being object st x in dom f holds g.x in f.x by CARD_3:def 5;
rng g c= YY
proof
let y be object;
assume y in rng g;
then consider z being object such that
A10: z in dom g and
A11: y = g.z by FUNCT_1:def 3;
f.z = YY by A2,A8,A10;
hence thesis by A8,A9,A10,A11;
end;
hence thesis by A1,A7,A8,FUNCT_2:def 2;
end;
hence thesis by Def4;
end;
registration
let X be set;
let Y be non empty RelStr;
cluster Y|^X -> non empty;
coherence
proof
set f = the Function of X, the carrier of Y;
f in Funcs (X, the carrier of Y) by FUNCT_2:8;
hence thesis by Th28;
end;
end;
Lm5: for X be set, Y be non empty RelStr for x be Element of Y|^X holds x in
the carrier of product (X --> Y) & x is Function of X, the carrier of Y
proof
let X be set, Y be non empty RelStr, x be Element of Y|^X;
x in the carrier of Y|^X;
then x in Funcs (X, the carrier of Y) by Th28;
hence thesis by FUNCT_2:66;
end;
registration
let X be set;
let Y be reflexive non empty RelStr;
cluster Y|^X -> reflexive;
coherence
proof
per cases;
suppose
X is empty;
hence thesis by Th26;
end;
suppose
X is non empty;
then reconsider X as non empty set;
for x being Element of Y|^X holds x <= x
proof
let x be Element of Y|^X;
reconsider x1 = x as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Element of product (X --> Y);
A1: ex f,g being Function st f = x9 & g = x9 &
for i be object st i in X
ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi
= g.i & xi <= yi
proof
take x1, x1;
thus x1 = x9 & x1 = x9;
let i be object;
assume i in X;
then reconsider i as Element of X;
take R = (X --> Y).i;
reconsider xi = x1.i, yi = x1.i as Element of R;
take xi, yi;
reconsider xi1 = xi, yi1 = xi as Element of Y;
xi1 <= yi1;
hence thesis;
end;
x in the carrier of product (X --> Y);
then x9 in product Carrier (X --> Y) by Def4;
hence thesis by A1,Def4;
end;
hence thesis by YELLOW_0:def 1;
end;
end;
end;
registration
let Y be non empty RelStr;
cluster Y|^{} -> 1-element;
coherence by Th26;
end;
registration
let Y be non empty reflexive RelStr;
cluster Y|^{} -> with_infima with_suprema antisymmetric;
coherence;
end;
registration
let X be set;
let Y be transitive non empty RelStr;
cluster Y|^X -> transitive;
coherence
proof
set IT = Y|^X;
now
let x,y,z be Element of IT;
reconsider x1 = x, y1 = y, z1 = z as Element of product (X --> Y);
assume that
A1: x <= y and
A2: y <= z;
y1 in the carrier of product (X --> Y);
then y1 in product Carrier (X --> Y) by Def4;
then consider f1,g1 being Function such that
A3: f1 = y1 & g1 = z1 and
A4: for i be object st i in X ex R being RelStr, xi,yi being Element
of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A2,Def4;
x1 in the carrier of product (X --> Y);
then
A5: x1 in product Carrier (X --> Y) by Def4;
then consider f,g being Function such that
A6: f = x1 & g = y1 and
A7: for i be object st i in X ex R being RelStr, xi,yi being Element of
R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi by A1,Def4;
ex f2,g2 being Function st f2 = x1 & g2 = z1 & for i be object st i in
X ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f2.i &
yi = g2.i & xi <= yi
proof
reconsider f2 = x, g2 = z as Function of X, the carrier of Y by Lm5;
take f2, g2;
thus f2 = x1 & g2 = z1;
let i be object;
assume
A8: i in X;
then reconsider X as non empty set;
reconsider i as Element of X by A8;
reconsider R = (X --> Y).i as RelStr;
reconsider xi = f2.i, yi = g2.i as Element of R by FUNCT_2:5;
take R, xi, yi;
(ex R1 being RelStr, xi1,yi1 being Element of R1 st R1 = ( X -->
Y).i & xi1 = f.i & yi1 = g.i & xi1 <= yi1 )& ex R2 being RelStr, xi2,yi2 being
Element of R2 st R2 = ( X --> Y).i & xi2 = f1.i & yi2 = g1.i & xi2 <= yi2 by A7
,A4;
hence thesis by A6,A3,YELLOW_0:def 2;
end;
hence x <= z by A5,Def4;
end;
hence thesis by YELLOW_0:def 2;
end;
end;
registration
let X be set;
let Y be antisymmetric non empty RelStr;
cluster Y|^X -> antisymmetric;
coherence
proof
set IT = Y|^X;
now
let x,y be Element of IT;
reconsider x19 = x, y19 = y as Function of X, the carrier of Y by Lm5;
reconsider x1 = x, y1 = y as Element of product (X --> Y);
assume that
A1: x <= y and
A2: y <= x;
y1 in the carrier of product (X --> Y);
then y1 in product Carrier (X --> Y) by Def4;
then consider f1,g1 being Function such that
A3: f1 = y1 & g1 = x1 and
A4: for i be object st i in X ex R being RelStr, xi,yi being Element
of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A2,Def4;
x1 in the carrier of product (X --> Y);
then x1 in product Carrier (X --> Y) by Def4;
then consider f,g being Function such that
A5: f = x1 & g = y1 and
A6: for i be object st i in X ex R being RelStr, xi,yi being Element of
R st R = (X --> Y).i & xi = f.i & yi = g.i & xi <= yi by A1,Def4;
A7: now
let i be object;
assume
A8: i in X;
then consider R2 being RelStr, xi2,yi2 being Element of R2 such that
A9: R2 = (X --> Y).i and
A10: xi2 = f1.i & yi2 = g1.i & xi2 <= yi2 by A4;
A11: Y = R2 by A8,A9,FUNCOP_1:7;
consider R1 being RelStr, xi1,yi1 being Element of R1 such that
A12: R1 = (X --> Y).i and
A13: xi1 = f.i & yi1 = g.i & xi1 <= yi1 by A6,A8;
Y = R1 by A8,A12,FUNCOP_1:7;
hence x19.i = y19.i by A5,A3,A13,A10,A11,ORDERS_2:2;
end;
dom x19 = X & dom y19 = X by FUNCT_2:def 1;
hence x = y by A7,FUNCT_1:2;
end;
hence thesis by YELLOW_0:def 3;
end;
end;
registration
let X be non empty set;
let Y be non empty with_infima antisymmetric RelStr;
cluster Y|^X -> with_infima;
coherence
proof
set IT = Y|^X;
let x, y be Element of IT;
reconsider y9 = y as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Function of X, the carrier of Y by Lm5;
defpred P[object, object] means
ex xa, ya be Element of Y st xa = x9.$1 & ya =
y9.$1 & $2 = xa "/\" ya;
A1: for x be object st x in X
ex y be object st y in the carrier of Y & P[x,y]
proof
let a be object;
assume a in X;
then reconsider xa = x9.a, ya = y9.a as Element of Y by FUNCT_2:5;
take y = xa "/\" ya;
thus y in the carrier of Y;
take xa, ya;
thus thesis;
end;
consider f be Function of X, the carrier of Y such that
A2: for a be object st a in X holds P[a,f.a] from FUNCT_2:sch 1(A1);
f in Funcs (X, the carrier of Y) by FUNCT_2:8;
then reconsider z = f as Element of IT by Th28;
take z;
A3: z <= y
proof
reconsider y1 = y, z1 = z as Element of product (X --> Y);
A4: ex f,g being Function st f = z1 & g = y1 &
for i be object st i in X
ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi
= g.i & xi <= yi
proof
take f, y9;
thus f = z1 & y9 = y1;
let i be object;
assume i in X;
then reconsider i as Element of X;
reconsider R = (X --> Y).i as RelStr;
reconsider xi = f.i, yi = y9.i as Element of R;
take R, xi, yi;
R = Y & ex xa, ya be Element of Y st xa = x9.i & ya = y9.i & f. i
= xa "/\" ya by A2;
hence thesis by YELLOW_0:23;
end;
z1 in the carrier of product (X --> Y);
then z1 in product Carrier (X --> Y) by Def4;
hence thesis by A4,Def4;
end;
A5: for z9 being Element of IT st z9 <= x & z9 <= y holds z9 <= z
proof
let z9 be Element of IT;
assume that
A6: z9 <= x and
A7: z9 <= y;
z9 <= z
proof
reconsider z2 = z9, z3 = z, z4 = y, z5 = x as Element of product (X
--> Y);
reconsider J = z2, K = z3 as Function of X, the carrier of Y by Lm5;
z9 in the carrier of product (X --> Y);
then
A8: z2 in product Carrier (X --> Y) by Def4;
then consider f1,g1 being Function such that
A9: f1 = z2 & g1 = z5 and
A10: for i be object st i in X ex R being RelStr, xi,yi being Element
of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A6,Def4;
consider f2,g2 being Function such that
A11: f2 = z2 & g2 = z4 and
A12: for i be object st i in X ex R being RelStr, xi,yi being Element
of R st R = (X --> Y).i & xi = f2.i & yi = g2.i & xi <= yi by A7,A8,Def4;
ex f,g being Function st f = z2 & g = z3 &
for i be object st i in X
ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi
= g.i & xi <= yi
proof
take J, K;
thus J = z2 & K = z3;
let i be object;
assume i in X;
then reconsider i as Element of X;
reconsider R = (X --> Y).i as RelStr;
reconsider xi = J.i, yi = K.i as Element of R;
take R, xi, yi;
A13: R = Y & ex xa, ya be Element of Y st xa = x9.i & ya = y9.i & f.
i = xa "/\" ya by A2;
(ex R1 being RelStr, xi1,yi1 being Element of R1 st R1 = ( X
--> Y).i & xi1 = f1.i & yi1 = g1.i & xi1 <= yi1 )& ex R2 being RelStr, xi2,yi2
being Element of R2 st R2 = ( X --> Y).i & xi2 = f2.i & yi2 = g2.i & xi2 <= yi2
by A10,A12;
hence thesis by A9,A11,A13,YELLOW_0:23;
end;
hence thesis by A8,Def4;
end;
hence thesis;
end;
z <= x
proof
reconsider x1 = x, z1 = z as Element of product (X --> Y);
A14: ex f,g being Function st f = z1 & g = x1 &
for i be object st i in X ex
R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g
.i & xi <= yi
proof
take f, x9;
thus f = z1 & x9 = x1;
let i be object;
assume i in X;
then reconsider i as Element of X;
reconsider R = (X --> Y).i as RelStr;
reconsider xi = f.i, yi = x9.i as Element of R;
take R, xi, yi;
R = Y & ex xa, ya be Element of Y st xa = x9.i & ya = y9.i & f. i
= xa "/\" ya by A2;
hence thesis by YELLOW_0:23;
end;
z1 in the carrier of product (X --> Y);
then z1 in product Carrier (X --> Y) by Def4;
hence thesis by A14,Def4;
end;
hence thesis by A3,A5;
end;
end;
registration
let X be non empty set;
let Y be non empty with_suprema antisymmetric RelStr;
cluster Y|^X -> with_suprema;
coherence
proof
set IT = Y|^X;
let x, y be Element of IT;
reconsider y9 = y as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Function of X, the carrier of Y by Lm5;
defpred P[object, object] means
ex xa, ya be Element of Y st xa = x9.$1 & ya =
y9.$1 & $2 = xa "\/" ya;
A1: for x be object st x in X
ex y be object st y in the carrier of Y & P[x,y]
proof
let a be object;
assume a in X;
then reconsider xa = x9.a, ya = y9.a as Element of Y by FUNCT_2:5;
take y = xa "\/" ya;
thus y in the carrier of Y;
take xa, ya;
thus thesis;
end;
consider f be Function of X, the carrier of Y such that
A2: for a be object st a in X holds P[a,f.a] from FUNCT_2:sch 1(A1);
f in Funcs (X, the carrier of Y) by FUNCT_2:8;
then reconsider z = f as Element of IT by Th28;
take z;
A3: y <= z
proof
reconsider y1 = y, z1 = z as Element of product (X --> Y);
A4: ex f,g being Function st f = y1 & g = z1 &
for i be object st i in X
ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi
= g.i & xi <= yi
proof
take y9, f;
thus y9 = y1 & f = z1;
let i be object;
assume i in X;
then reconsider i as Element of X;
reconsider R = (X --> Y).i as RelStr;
reconsider yi = f.i, xi = y9.i as Element of R;
take R, xi, yi;
R = Y & ex xa, ya be Element of Y st xa = x9.i & ya = y9.i & f. i
= xa "\/" ya by A2;
hence thesis by YELLOW_0:22;
end;
y1 in the carrier of product (X --> Y);
then y1 in product Carrier (X --> Y) by Def4;
hence thesis by A4,Def4;
end;
A5: for z9 being Element of IT st z9 >= x & z9 >= y holds z9 >= z
proof
let z9 be Element of IT;
assume that
A6: z9 >= x and
A7: z9 >= y;
z9 >= z
proof
reconsider z2 = z9, z3 = z, z4 = y, z5 = x as Element of product (X
--> Y);
z4 in the carrier of product (X --> Y);
then z4 in product Carrier (X --> Y) by Def4;
then consider f2,g2 being Function such that
A8: f2 = z4 & g2 = z2 and
A9: for i be object st i in X ex R being RelStr, xi,yi being Element
of R st R = (X --> Y).i & xi = f2.i & yi = g2.i & xi <= yi by A7,Def4;
reconsider K = z3, J = z2 as Function of X, the carrier of Y by Lm5;
z5 in the carrier of product (X --> Y);
then z5 in product Carrier (X --> Y) by Def4;
then consider f1,g1 being Function such that
A10: f1 = z5 & g1 = z2 and
A11: for i be object st i in X ex R being RelStr, xi,yi being Element
of R st R = (X --> Y).i & xi = f1.i & yi = g1.i & xi <= yi by A6,Def4;
A12: ex f,g being Function st f = z3 & g = z2 &
for i be object st i in X
ex R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi
= g.i & xi <= yi
proof
take K, J;
thus K = z3 & J = z2;
let i be object;
assume i in X;
then reconsider i as Element of X;
reconsider R = (X --> Y).i as RelStr;
reconsider yi = J.i, xi = K.i as Element of R;
take R, xi, yi;
A13: R = Y & ex xa, ya be Element of Y st xa = x9.i & ya = y9.i & f.
i = xa "\/" ya by A2;
(ex R1 being RelStr, xi1,yi1 being Element of R1 st R1 = ( X
--> Y).i & xi1 = f1.i & yi1 = g1.i & xi1 <= yi1 )& ex R2 being RelStr, xi2,yi2
being Element of R2 st R2 = ( X --> Y).i & xi2 = f2.i & yi2 = g2.i & xi2 <= yi2
by A11,A9;
hence thesis by A10,A8,A13,YELLOW_0:22;
end;
z3 in the carrier of product (X --> Y);
then z3 in product Carrier (X --> Y) by Def4;
hence thesis by A12,Def4;
end;
hence thesis;
end;
x <= z
proof
reconsider x1 = x, z1 = z as Element of product (X --> Y);
A14: ex f,g being Function st f = x1 & g = z1 &
for i be object st i in X ex
R being RelStr, xi,yi being Element of R st R = (X --> Y).i & xi = f.i & yi = g
.i & xi <= yi
proof
take x9,f;
thus x9 = x1 & f = z1;
let i be object;
assume i in X;
then reconsider i as Element of X;
reconsider R = (X --> Y).i as RelStr;
reconsider yi = f.i, xi = x9.i as Element of R;
take R, xi, yi;
R = Y & ex xa, ya be Element of Y st xa = x9.i & ya = y9.i & f. i
= xa "\/" ya by A2;
hence thesis by YELLOW_0:22;
end;
x1 in the carrier of product (X --> Y);
then x1 in product Carrier (X --> Y) by Def4;
hence thesis by A14,Def4;
end;
hence thesis by A3,A5;
end;
end;
definition
let S,T be RelStr;
func MonMaps (S,T) -> strict full SubRelStr of T|^the carrier of S means
for f being Function of S,T holds f in the carrier of it iff f in Funcs (the
carrier of S, the carrier of T) & f is monotone;
existence
proof
set X = MonFuncs (S,T);
X c= Funcs (the carrier of S, the carrier of T) by ORDERS_3:11;
then reconsider X as Subset of T|^the carrier of S by Th28;
take SX = subrelstr X;
let f be Function of S,T;
hereby
assume f in the carrier of SX;
then f in X by YELLOW_0:def 15;
then
ex f9 be Function of S, T st f9 = f & f9 in Funcs (the carrier of S,
the carrier of T) & f9 is monotone by ORDERS_3:def 6;
hence f in Funcs (the carrier of S, the carrier of T) & f is monotone;
end;
assume f in Funcs (the carrier of S, the carrier of T) & f is monotone;
then f in X by ORDERS_3:def 6;
hence thesis by YELLOW_0:def 15;
end;
uniqueness
proof
let A1, A2 be strict full SubRelStr of T|^the carrier of S;
assume that
A1: for f being Function of S,T holds f in the carrier of A1 iff f in
Funcs (the carrier of S, the carrier of T) & f is monotone and
A2: for f being Function of S,T holds f in the carrier of A2 iff f in
Funcs (the carrier of S, the carrier of T) & f is monotone;
the carrier of A2 c= the carrier of T|^the carrier of S by YELLOW_0:def 13;
then
A3: the carrier of A2 c= Funcs (the carrier of S, the carrier of T) by Th28;
A4: the carrier of A2 c= the carrier of A1
proof
let a be object;
assume
A5: a in the carrier of A2;
then reconsider f = a as Function of S, T by A3,FUNCT_2:66;
f is monotone by A2,A5;
hence thesis by A1,A3,A5;
end;
the carrier of A1 c= the carrier of T|^the carrier of S by YELLOW_0:def 13;
then
A6: the carrier of A1 c= Funcs (the carrier of S, the carrier of T) by Th28;
the carrier of A1 c= the carrier of A2
proof
let a be object;
assume
A7: a in the carrier of A1;
then reconsider f = a as Function of S, T by A6,FUNCT_2:66;
f is monotone by A1,A7;
hence thesis by A2,A6,A7;
end;
then the carrier of A1 = the carrier of A2 by A4;
hence thesis by YELLOW_0:57;
end;
end;