:: YELLOW_1 semantic presentation
begin
registration
let L be Lattice;
cluster LattPOSet L -> with_suprema with_infima ;
coherence
( LattPOSet L is with_suprema & LattPOSet L is with_infima ) by LATTICE3:11;
end;
registration
let L be upper-bounded Lattice;
cluster LattPOSet L -> upper-bounded ;
coherence
LattPOSet L is upper-bounded
proof
ex x being Element of (LattPOSet L) st x is_>=_than the carrier of (LattPOSet L)
proof
take x = Top (LattPOSet L); ::_thesis: x is_>=_than the carrier of (LattPOSet L)
consider z being 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__::_thesis:_for_b9_being_Element_of_(LattPOSet_L)_st_b9_is_<=_than_{}_holds_
z9_>=_b9
let b9 be Element of (LattPOSet L); ::_thesis: ( b9 is_<=_than {} implies z9 >= b9 )
reconsider b = b9 as Element of L ;
assume b9 is_<=_than {} ; ::_thesis: z9 >= b9
A4: ( b % = b & z % = z ) ;
b [= z by A2, LATTICES:19;
hence z9 >= b9 by A4, LATTICE3:7; ::_thesis: verum
end;
z9 is_<=_than {} by YELLOW_0:6;
then A5: z9 = "/\" ({},(LattPOSet L)) by A3, YELLOW_0:31;
now__::_thesis:_for_a_being_Element_of_(LattPOSet_L)_st_a_in_the_carrier_of_(LattPOSet_L)_holds_
a_<=_x
reconsider x9 = x as Element of L ;
let a be Element of (LattPOSet L); ::_thesis: ( a in the carrier of (LattPOSet L) implies a <= x )
assume a in the carrier of (LattPOSet L) ; ::_thesis: a <= x
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; ::_thesis: verum
end;
hence x is_>=_than the carrier of (LattPOSet L) by LATTICE3:def_9; ::_thesis: verum
end;
hence LattPOSet L is upper-bounded by YELLOW_0:def_5; ::_thesis: verum
end;
end;
registration
let L be lower-bounded Lattice;
cluster LattPOSet L -> lower-bounded ;
coherence
LattPOSet L is lower-bounded
proof
ex x being Element of (LattPOSet L) st x is_<=_than the carrier of (LattPOSet L)
proof
take x = Bottom (LattPOSet L); ::_thesis: x is_<=_than the carrier of (LattPOSet L)
consider z being 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__::_thesis:_for_b9_being_Element_of_(LattPOSet_L)_st_b9_is_>=_than_{}_holds_
z9_<=_b9
let b9 be Element of (LattPOSet L); ::_thesis: ( b9 is_>=_than {} implies z9 <= b9 )
reconsider b = b9 as Element of L ;
assume b9 is_>=_than {} ; ::_thesis: z9 <= b9
A4: ( b % = b & z % = z ) ;
z [= b by A2, LATTICES:16;
hence z9 <= b9 by A4, LATTICE3:7; ::_thesis: verum
end;
z9 is_>=_than {} by YELLOW_0:6;
then A5: z9 = "\/" ({},(LattPOSet L)) by A3, YELLOW_0:30;
now__::_thesis:_for_a_being_Element_of_(LattPOSet_L)_st_a_in_the_carrier_of_(LattPOSet_L)_holds_
x_<=_a
reconsider x9 = x as Element of L ;
let a be Element of (LattPOSet L); ::_thesis: ( a in the carrier of (LattPOSet L) implies x <= a )
assume a in the carrier of (LattPOSet L) ; ::_thesis: x <= a
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; ::_thesis: verum
end;
hence x is_<=_than the carrier of (LattPOSet L) by LATTICE3:def_8; ::_thesis: verum
end;
hence LattPOSet L is lower-bounded by YELLOW_0:def_4; ::_thesis: verum
end;
end;
registration
let L be complete Lattice;
cluster LattPOSet L -> complete ;
coherence
LattPOSet L is complete
proof
for X being set ex a being 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 ; ::_thesis: ex a being Element of (LattPOSet L) st
( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )
take a = "\/" (X,(LattPOSet L)); ::_thesis: ( X is_<=_than a & ( for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b ) )
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; ::_thesis: for b being Element of (LattPOSet L) st X is_<=_than b holds
a <= b
let b be Element of (LattPOSet L); ::_thesis: ( X is_<=_than b implies a <= b )
reconsider b9 = b as Element of L ;
assume X is_<=_than b ; ::_thesis: a <= 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 a <= b by A1, LATTICE3:7; ::_thesis: verum
end;
hence LattPOSet L is complete by LATTICE3:def_12; ::_thesis: verum
end;
end;
definition
let X be set ;
:: original: RelIncl
redefine func RelIncl X -> Order of X;
coherence
RelIncl X is Order of X
proof
now__::_thesis:_for_x_being_set_st_x_in_RelIncl_X_holds_
x_in_[:X,X:]
let x be set ; ::_thesis: ( x in RelIncl X implies x in [:X,X:] )
assume A1: x in RelIncl X ; ::_thesis: x in [:X,X:]
then consider y, z being set such that
A2: x = [y,z] by RELAT_1:def_1;
z in field (RelIncl X) by A1, A2, RELAT_1:15;
then A3: z in X by WELLORD2:def_1;
y in field (RelIncl X) by A1, A2, RELAT_1:15;
then y in X by WELLORD2:def_1;
hence x in [:X,X:] by A2, A3, ZFMISC_1:87; ::_thesis: verum
end;
then reconsider R = RelIncl X as Relation of X by TARSKI:def_3;
( field R = X & R is reflexive ) by WELLORD2:def_1;
then R is_reflexive_in X by RELAT_2:def_9;
then dom R = X by ORDERS_1:13;
hence RelIncl X is Order of X by PARTFUN1:def_2; ::_thesis: verum
end;
end;
definition
let X be set ;
func InclPoset X -> strict RelStr equals :: YELLOW_1:def 1
RelStr(# X,(RelIncl X) #);
correctness
coherence
RelStr(# X,(RelIncl X) #) is strict RelStr ;
;
end;
:: deftheorem defines InclPoset YELLOW_1:def_1_:_
for X being set holds InclPoset X = RelStr(# X,(RelIncl X) #);
registration
let X be set ;
cluster InclPoset X -> strict reflexive transitive antisymmetric ;
coherence
( InclPoset X is reflexive & InclPoset X is antisymmetric & InclPoset X is transitive ) ;
end;
registration
let X be non empty set ;
cluster InclPoset X -> non empty strict ;
coherence
not InclPoset X is empty ;
end;
theorem :: YELLOW_1:1
for X being set holds
( the carrier of (InclPoset X) = X & the InternalRel of (InclPoset X) = RelIncl X ) ;
definition
let X be set ;
func BoolePoset X -> strict RelStr equals :: YELLOW_1:def 2
LattPOSet (BooleLatt X);
correctness
coherence
LattPOSet (BooleLatt X) is strict RelStr ;
;
end;
:: deftheorem defines BoolePoset YELLOW_1:def_2_:_
for X being set holds BoolePoset X = LattPOSet (BooleLatt X);
registration
let X be set ;
cluster BoolePoset X -> non empty strict reflexive transitive antisymmetric ;
coherence
( not BoolePoset X is empty & BoolePoset X is reflexive & BoolePoset X is antisymmetric & BoolePoset X is transitive ) ;
end;
registration
let X be set ;
cluster BoolePoset X -> strict complete ;
coherence
BoolePoset X is complete ;
end;
theorem Th2: :: YELLOW_1:2
for X being set
for x, y being Element of (BoolePoset X) holds
( x <= y iff x c= y )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x <= y iff x c= y )
let x, y be Element of (BoolePoset X); ::_thesis: ( x <= y iff x c= y )
reconsider x9 = x, y9 = y as Element of (BooleLatt X) ;
thus ( x <= y implies x c= y ) ::_thesis: ( x c= y implies x <= y )
proof
assume x <= y ; ::_thesis: x c= y
then x9 % <= y9 % ;
then x9 [= y9 by LATTICE3:7;
hence x c= y by LATTICE3:2; ::_thesis: verum
end;
assume x c= y ; ::_thesis: x <= y
then x9 [= y9 by LATTICE3:2;
then x9 % <= y9 % by LATTICE3:7;
hence x <= y ; ::_thesis: verum
end;
theorem Th3: :: YELLOW_1:3
for X being non empty set
for x, y being Element of (InclPoset X) holds
( x <= y iff x c= y )
proof
let X be non empty set ; ::_thesis: for x, y being Element of (InclPoset X) holds
( x <= y iff x c= y )
let x, y be Element of (InclPoset X); ::_thesis: ( x <= y iff x c= y )
thus ( x <= y implies x c= y ) ::_thesis: ( x c= y implies x <= y )
proof
assume x <= y ; ::_thesis: x c= y
then [x,y] in the InternalRel of (InclPoset X) by ORDERS_2:def_5;
hence x c= y by WELLORD2:def_1; ::_thesis: verum
end;
thus ( x c= y implies x <= y ) ::_thesis: verum
proof
assume x c= y ; ::_thesis: x <= y
then [x,y] in RelIncl X by WELLORD2:def_1;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
end;
theorem Th4: :: YELLOW_1:4
for X being set holds BoolePoset X = InclPoset (bool X)
proof
let X be set ; ::_thesis: BoolePoset X = InclPoset (bool X)
set B = BoolePoset X;
the carrier of (BoolePoset X) = bool X by LATTICE3:def_1;
then reconsider In = the InternalRel of (BoolePoset X) as Relation of (bool X) ;
for x being set st x in bool X holds
ex y being set st [x,y] in In
proof
let x be set ; ::_thesis: ( x in bool X implies ex y being set st [x,y] in In )
assume x in bool X ; ::_thesis: ex y being set st [x,y] in In
then reconsider x9 = x as Element of (BoolePoset X) by LATTICE3:def_1;
take y = x9; ::_thesis: [x,y] in In
x9 <= y ;
hence [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then A1: dom In = bool X by RELSET_1:9;
A2: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_bool_X_&_Z_in_bool_X_holds_
(_(_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_implies_Y_c=_Z_)_&_(_Y_c=_Z_implies_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_)_)
let Y, Z be set ; ::_thesis: ( Y in bool X & Z in bool X implies ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ) )
assume ( Y in bool X & Z in bool X ) ; ::_thesis: ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) )
then reconsider Y9 = Y, Z9 = Z as Element of (BoolePoset X) by LATTICE3:def_1;
thus ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) ::_thesis: ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) )
proof
assume [Y,Z] in the InternalRel of (BoolePoset X) ; ::_thesis: Y c= Z
then Y9 <= Z9 by ORDERS_2:def_5;
hence Y c= Z by Th2; ::_thesis: verum
end;
thus ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ::_thesis: verum
proof
assume Y c= Z ; ::_thesis: [Y,Z] in the InternalRel of (BoolePoset X)
then Y9 <= Z9 by Th2;
hence [Y,Z] in the InternalRel of (BoolePoset X) by ORDERS_2:def_5; ::_thesis: verum
end;
end;
for y being set st y in bool X holds
ex x being set st [x,y] in In
proof
let y be set ; ::_thesis: ( y in bool X implies ex x being set st [x,y] in In )
assume y in bool X ; ::_thesis: ex x being set st [x,y] in In
then reconsider y9 = y as Element of (BoolePoset X) by LATTICE3:def_1;
take x = y9; ::_thesis: [x,y] in In
x <= y9 ;
hence [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then field the InternalRel of (BoolePoset X) = (bool X) \/ (bool X) by A1, RELSET_1:10;
then the InternalRel of (BoolePoset X) = RelIncl (bool X) by A2, WELLORD2:def_1;
hence BoolePoset X = InclPoset (bool X) by LATTICE3:def_1; ::_thesis: verum
end;
theorem :: YELLOW_1:5
for X being set
for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X
proof
let X be set ; ::_thesis: for Y being Subset-Family of X holds InclPoset Y is full SubRelStr of BoolePoset X
set L = BoolePoset X;
let Y be Subset-Family of X; ::_thesis: InclPoset Y is full SubRelStr of BoolePoset X
reconsider Y9 = Y as Subset of (BoolePoset X) by LATTICE3:def_1;
the carrier of (BoolePoset X) = bool X by LATTICE3:def_1;
then reconsider In = the InternalRel of (BoolePoset X) as Relation of (bool X) ;
for x being set st x in bool X holds
ex y being set st [x,y] in In
proof
let x be set ; ::_thesis: ( x in bool X implies ex y being set st [x,y] in In )
assume x in bool X ; ::_thesis: ex y being set st [x,y] in In
then reconsider x9 = x as Element of (BoolePoset X) by LATTICE3:def_1;
take y = x9; ::_thesis: [x,y] in In
x9 <= y ;
hence [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then A1: dom In = bool X by RELSET_1:9;
A2: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_bool_X_&_Z_in_bool_X_holds_
(_(_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_implies_Y_c=_Z_)_&_(_Y_c=_Z_implies_[Y,Z]_in_the_InternalRel_of_(BoolePoset_X)_)_)
let Y, Z be set ; ::_thesis: ( Y in bool X & Z in bool X implies ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ) )
assume ( Y in bool X & Z in bool X ) ; ::_thesis: ( ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) )
then reconsider Y9 = Y, Z9 = Z as Element of (BoolePoset X) by LATTICE3:def_1;
thus ( [Y,Z] in the InternalRel of (BoolePoset X) implies Y c= Z ) ::_thesis: ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) )
proof
assume [Y,Z] in the InternalRel of (BoolePoset X) ; ::_thesis: Y c= Z
then Y9 <= Z9 by ORDERS_2:def_5;
hence Y c= Z by Th2; ::_thesis: verum
end;
thus ( Y c= Z implies [Y,Z] in the InternalRel of (BoolePoset X) ) ::_thesis: verum
proof
assume Y c= Z ; ::_thesis: [Y,Z] in the InternalRel of (BoolePoset X)
then Y9 <= Z9 by Th2;
hence [Y,Z] in the InternalRel of (BoolePoset X) by ORDERS_2:def_5; ::_thesis: verum
end;
end;
for y being set st y in bool X holds
ex x being set st [x,y] in In
proof
let y be set ; ::_thesis: ( y in bool X implies ex x being set st [x,y] in In )
assume y in bool X ; ::_thesis: ex x being set st [x,y] in In
then reconsider y9 = y as Element of (BoolePoset X) by LATTICE3:def_1;
take x = y9; ::_thesis: [x,y] in In
x <= y9 ;
hence [x,y] in In by ORDERS_2:def_5; ::_thesis: verum
end;
then field the InternalRel of (BoolePoset X) = (bool X) \/ (bool X) by A1, RELSET_1:10;
then A3: the InternalRel of (BoolePoset X) = RelIncl (bool X) by A2, WELLORD2:def_1;
RelStr(# Y9,( the InternalRel of (BoolePoset X) |_2 Y9) #) is full SubRelStr of BoolePoset X by YELLOW_0:56;
hence InclPoset Y is full SubRelStr of BoolePoset X by A3, WELLORD2:7; ::_thesis: verum
end;
theorem :: YELLOW_1:6
for X being non empty set st InclPoset X is with_suprema holds
for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y
proof
let X be non empty set ; ::_thesis: ( InclPoset X is with_suprema implies for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y )
assume A1: InclPoset X is with_suprema ; ::_thesis: for x, y being Element of (InclPoset X) holds x \/ y c= x "\/" y
let x, y be Element of (InclPoset X); ::_thesis: x \/ y c= x "\/" y
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 x \/ y c= x "\/" y by A2, XBOOLE_1:8; ::_thesis: verum
end;
theorem :: YELLOW_1:7
for X being non empty set st InclPoset X is with_infima holds
for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y
proof
let X be non empty set ; ::_thesis: ( InclPoset X is with_infima implies for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y )
assume A1: InclPoset X is with_infima ; ::_thesis: for x, y being Element of (InclPoset X) holds x "/\" y c= x /\ y
let x, y be Element of (InclPoset X); ::_thesis: x "/\" y c= x /\ y
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 x "/\" y c= x /\ y by A2, XBOOLE_1:19; ::_thesis: verum
end;
theorem Th8: :: YELLOW_1:8
for X being non empty set
for x, y being Element of (InclPoset X) st x \/ y in X holds
x "\/" y = x \/ y
proof
let X be non empty set ; ::_thesis: for x, y being Element of (InclPoset X) st x \/ y in X holds
x "\/" y = x \/ y
let x, y be Element of (InclPoset X); ::_thesis: ( x \/ y in X implies x "\/" y = x \/ y )
assume x \/ y in X ; ::_thesis: x "\/" y = x \/ y
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__::_thesis:_for_c_being_Element_of_(InclPoset_X)_st_x_<=_c_&_y_<=_c_holds_
z_<=_c
let c be Element of (InclPoset X); ::_thesis: ( x <= c & y <= c implies z <= c )
assume ( x <= c & y <= c ) ; ::_thesis: z <= c
then ( x c= c & y c= c ) by Th3;
then z c= c by XBOOLE_1:8;
hence z <= c by Th3; ::_thesis: verum
end;
x c= z by XBOOLE_1:7;
then x <= z by Th3;
hence x "\/" y = x \/ y by A1, A2, LATTICE3:def_13; ::_thesis: verum
end;
theorem Th9: :: YELLOW_1:9
for X being non empty set
for x, y being Element of (InclPoset X) st x /\ y in X holds
x "/\" y = x /\ y
proof
let X be non empty set ; ::_thesis: for x, y being Element of (InclPoset X) st x /\ y in X holds
x "/\" y = x /\ y
let x, y be Element of (InclPoset X); ::_thesis: ( x /\ y in X implies x "/\" y = x /\ y )
assume x /\ y in X ; ::_thesis: x "/\" y = x /\ y
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__::_thesis:_for_c_being_Element_of_(InclPoset_X)_st_c_<=_x_&_c_<=_y_holds_
c_<=_z
let c be Element of (InclPoset X); ::_thesis: ( c <= x & c <= y implies c <= z )
assume ( c <= x & c <= y ) ; ::_thesis: c <= z
then ( c c= x & c c= y ) by Th3;
then c c= z by XBOOLE_1:19;
hence c <= z by Th3; ::_thesis: verum
end;
z c= x by XBOOLE_1:17;
then z <= x by Th3;
hence x "/\" y = x /\ y by A1, A2, LATTICE3:def_14; ::_thesis: verum
end;
theorem :: YELLOW_1:10
for L being RelStr st ( for x, y being 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 ; ::_thesis: ( ( for x, y being Element of L holds
( x <= y iff x c= y ) ) implies the InternalRel of L = RelIncl the carrier of L )
assume A1: for x, y being Element of L holds
( x <= y iff x c= y ) ; ::_thesis: the InternalRel of L = RelIncl the carrier of L
A2: now__::_thesis:_for_Y,_Z_being_set_st_Y_in_the_carrier_of_L_&_Z_in_the_carrier_of_L_holds_
(_(_[Y,Z]_in_the_InternalRel_of_L_implies_Y_c=_Z_)_&_(_Y_c=_Z_implies_[Y,Z]_in_the_InternalRel_of_L_)_)
let Y, Z be set ; ::_thesis: ( Y in the carrier of L & Z in the carrier of L implies ( ( [Y,Z] in the InternalRel of L implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of L ) ) )
assume ( Y in the carrier of L & Z in the carrier of L ) ; ::_thesis: ( ( [Y,Z] in the InternalRel of L implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of L ) )
then reconsider Y9 = Y, Z9 = Z as Element of L ;
thus ( [Y,Z] in the InternalRel of L implies Y c= Z ) ::_thesis: ( Y c= Z implies [Y,Z] in the InternalRel of L )
proof
assume [Y,Z] in the InternalRel of L ; ::_thesis: Y c= Z
then Y9 <= Z9 by ORDERS_2:def_5;
hence Y c= Z by A1; ::_thesis: verum
end;
thus ( Y c= Z implies [Y,Z] in the InternalRel of L ) ::_thesis: verum
proof
assume Y c= Z ; ::_thesis: [Y,Z] in the InternalRel of L
then Y9 <= Z9 by A1;
hence [Y,Z] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
end;
for x being set st x in the carrier of L holds
ex y being set st [x,y] in the InternalRel of L
proof
let x be set ; ::_thesis: ( x in the carrier of L implies ex y being set st [x,y] in the InternalRel of L )
assume x in the carrier of L ; ::_thesis: ex y being set st [x,y] in the InternalRel of L
then reconsider x9 = x as Element of L ;
take y = x9; ::_thesis: [x,y] in the InternalRel of L
x9 <= y by A1;
hence [x,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
then A3: dom the InternalRel of L = the carrier of L by RELSET_1:9;
for y being set st y in the carrier of L holds
ex x being set st [x,y] in the InternalRel of L
proof
let y be set ; ::_thesis: ( y in the carrier of L implies ex x being set st [x,y] in the InternalRel of L )
assume y in the carrier of L ; ::_thesis: ex x being set st [x,y] in the InternalRel of L
then reconsider y9 = y as Element of L ;
take x = y9; ::_thesis: [x,y] in the InternalRel of L
x <= y9 by A1;
hence [x,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
then field the InternalRel of L = the carrier of L \/ the carrier of L by A3, RELSET_1:10;
hence the InternalRel of L = RelIncl the carrier of L by A2, WELLORD2:def_1; ::_thesis: verum
end;
theorem :: YELLOW_1:11
for X being non empty set st ( for x, y being 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 ; ::_thesis: ( ( for x, y being set st x in X & y in X holds
x \/ y in X ) implies InclPoset X is with_suprema )
set L = InclPoset X;
assume A1: for x, y being set st x in X & y in X holds
x \/ y in X ; ::_thesis: InclPoset X is with_suprema
now__::_thesis:_for_a,_b_being_Element_of_(InclPoset_X)_holds_ex_sup_of_{a,b},_InclPoset_X
let a, b be Element of (InclPoset X); ::_thesis: ex_sup_of {a,b}, InclPoset X
ex c being Element of (InclPoset X) st
( {a,b} is_<=_than c & ( for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d ) )
proof
take c = a "\/" b; ::_thesis: ( {a,b} is_<=_than c & ( for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d ) )
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; ::_thesis: for d being Element of (InclPoset X) st {a,b} is_<=_than d holds
c <= d
let d be Element of (InclPoset X); ::_thesis: ( {a,b} is_<=_than d implies c <= d )
assume A4: {a,b} is_<=_than d ; ::_thesis: c <= d
b in {a,b} by TARSKI:def_2;
then b <= d by A4, LATTICE3:def_9;
then A5: b c= d by Th3;
a in {a,b} by TARSKI:def_2;
then a <= d by A4, LATTICE3:def_9;
then a c= d by Th3;
then a \/ b c= d by A5, XBOOLE_1:8;
then c c= d by A1, Th8;
hence c <= d by Th3; ::_thesis: verum
end;
hence ex_sup_of {a,b}, InclPoset X by YELLOW_0:15; ::_thesis: verum
end;
hence InclPoset X is with_suprema by YELLOW_0:20; ::_thesis: verum
end;
theorem :: YELLOW_1:12
for X being non empty set st ( for x, y being 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 ; ::_thesis: ( ( for x, y being set st x in X & y in X holds
x /\ y in X ) implies InclPoset X is with_infima )
set L = InclPoset X;
assume A1: for x, y being set st x in X & y in X holds
x /\ y in X ; ::_thesis: InclPoset X is with_infima
now__::_thesis:_for_a,_b_being_Element_of_(InclPoset_X)_holds_ex_inf_of_{a,b},_InclPoset_X
let a, b be Element of (InclPoset X); ::_thesis: ex_inf_of {a,b}, InclPoset X
ex c being Element of (InclPoset X) st
( {a,b} is_>=_than c & ( for d being Element of (InclPoset X) st {a,b} is_>=_than d holds
c >= d ) )
proof
take c = a "/\" b; ::_thesis: ( {a,b} is_>=_than c & ( for d being Element of (InclPoset X) st {a,b} is_>=_than d holds
c >= d ) )
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; ::_thesis: for d being Element of (InclPoset X) st {a,b} is_>=_than d holds
c >= d
let d be Element of (InclPoset X); ::_thesis: ( {a,b} is_>=_than d implies c >= d )
assume A4: {a,b} is_>=_than d ; ::_thesis: c >= d
b in {a,b} by TARSKI:def_2;
then d <= b by A4, LATTICE3:def_8;
then A5: d c= b by Th3;
a in {a,b} by TARSKI:def_2;
then d <= a by A4, LATTICE3:def_8;
then d c= a by Th3;
then d c= a /\ b by A5, XBOOLE_1:19;
then d c= c by A1, Th9;
hence c >= d by Th3; ::_thesis: verum
end;
hence ex_inf_of {a,b}, InclPoset X by YELLOW_0:16; ::_thesis: verum
end;
hence InclPoset X is with_infima by YELLOW_0:21; ::_thesis: verum
end;
theorem Th13: :: YELLOW_1:13
for X being non empty set st {} in X holds
Bottom (InclPoset X) = {}
proof
let X be non empty set ; ::_thesis: ( {} in X implies Bottom (InclPoset X) = {} )
assume {} in X ; ::_thesis: Bottom (InclPoset X) = {}
then reconsider a = {} as Element of (InclPoset X) ;
now__::_thesis:_for_b_being_Element_of_(InclPoset_X)_st_b_in_X_holds_
a_<=_b
let b be Element of (InclPoset X); ::_thesis: ( b in X implies a <= b )
assume b in X ; ::_thesis: a <= b
{} c= b by XBOOLE_1:2;
hence a <= b by Th3; ::_thesis: verum
end;
then a is_<=_than X by LATTICE3:def_8;
then InclPoset X is lower-bounded by YELLOW_0:def_4;
then ( {} is_<=_than a & ex_sup_of {} , InclPoset X ) by YELLOW_0:6, 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 ; ::_thesis: verum
end;
theorem Th14: :: YELLOW_1:14
for X being non empty set st union X in X holds
Top (InclPoset X) = union X
proof
let X be non empty set ; ::_thesis: ( union X in X implies Top (InclPoset X) = union X )
assume union X in X ; ::_thesis: Top (InclPoset X) = union X
then reconsider a = union X as Element of (InclPoset X) ;
now__::_thesis:_for_b_being_Element_of_(InclPoset_X)_st_b_in_X_holds_
b_<=_a
let b be Element of (InclPoset X); ::_thesis: ( b in X implies b <= a )
assume b in X ; ::_thesis: b <= a
b c= union X by ZFMISC_1:74;
hence b <= a by Th3; ::_thesis: verum
end;
then a is_>=_than X by LATTICE3:def_9;
then InclPoset X is upper-bounded by YELLOW_0:def_5;
then ( {} is_>=_than a & ex_inf_of {} , InclPoset X ) by YELLOW_0:6, 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, XBOOLE_0:def_10 ; ::_thesis: verum
end;
theorem :: YELLOW_1:15
for X being non empty set st InclPoset X is upper-bounded holds
union X in X
proof
let X be non empty set ; ::_thesis: ( InclPoset X is upper-bounded implies union X in X )
assume InclPoset X is upper-bounded ; ::_thesis: union X in X
then consider x being Element of (InclPoset X) such that
A1: x is_>=_than the carrier of (InclPoset X) by YELLOW_0:def_5;
now__::_thesis:_for_y_being_set_st_y_in_union_X_holds_
y_in_x
let y be set ; ::_thesis: ( y in union X implies y in x )
assume y in union X ; ::_thesis: y in x
then consider Y being set such that
A2: y in Y and
A3: Y in X by TARSKI:def_4;
reconsider Y = Y as Element of (InclPoset X) by A3;
Y <= x by A1, LATTICE3:def_9;
then Y c= x by Th3;
hence y in x by A2; ::_thesis: verum
end;
then A4: union X c= x by TARSKI:def_3;
( x in X & x c= union X ) by ZFMISC_1:74;
hence union X in X by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: YELLOW_1:16
for X being non empty set st InclPoset X is lower-bounded holds
meet X in X
proof
let X be non empty set ; ::_thesis: ( InclPoset X is lower-bounded implies meet X in X )
assume InclPoset X is lower-bounded ; ::_thesis: meet X in X
then consider x being Element of (InclPoset X) such that
A1: x is_<=_than the carrier of (InclPoset X) by YELLOW_0:def_4;
now__::_thesis:_for_y_being_set_st_y_in_x_holds_
y_in_meet_X
let y be set ; ::_thesis: ( y in x implies y in meet X )
assume A2: y in x ; ::_thesis: y in meet X
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
y_in_Y
let Y be set ; ::_thesis: ( Y in X implies y in Y )
assume Y in X ; ::_thesis: y in Y
then reconsider Y9 = Y as Element of (InclPoset X) ;
x <= Y9 by A1, LATTICE3:def_8;
then x c= Y by Th3;
hence y in Y by A2; ::_thesis: verum
end;
hence y in meet X by SETFAM_1:def_1; ::_thesis: verum
end;
then A3: x c= meet X by TARSKI:def_3;
( x in X & meet X c= x ) by SETFAM_1:3;
hence meet X in X by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm1: for X being set
for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x /\ y in bool X & x \/ y in bool X )
let x, y be Element of (BoolePoset X); ::_thesis: ( x /\ y in bool X & x \/ y in bool 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 ; ::_thesis: 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 x \/ y in bool X ; ::_thesis: verum
end;
theorem :: YELLOW_1:17
for X being set
for x, y being Element of (BoolePoset X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
proof
let X be set ; ::_thesis: for x, y being Element of (BoolePoset X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
let x, y be Element of (BoolePoset X); ::_thesis: ( x "\/" y = x \/ y & x "/\" y = x /\ y )
reconsider x = x, y = y as Element of (InclPoset (bool X)) by Th4;
( x "/\" y = x /\ y & x "\/" y = x \/ y ) by Lm1, Th8, Th9;
hence ( x "\/" y = x \/ y & x "/\" y = x /\ y ) by Th4; ::_thesis: verum
end;
theorem :: YELLOW_1:18
for X being set holds Bottom (BoolePoset X) = {}
proof
let X be set ; ::_thesis: Bottom (BoolePoset X) = {}
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 ; ::_thesis: verum
end;
theorem :: YELLOW_1:19
for X being set holds Top (BoolePoset X) = X
proof
let X be set ; ::_thesis: Top (BoolePoset X) = X
A1: Top (InclPoset (bool X)) = union (bool X) by Th14;
BoolePoset X = InclPoset (bool X) by Th4;
hence Top (BoolePoset X) = X by A1, ZFMISC_1:81; ::_thesis: verum
end;
theorem :: YELLOW_1:20
for X being set
for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y
proof
let X be set ; ::_thesis: for Y being non empty Subset of (BoolePoset X) holds inf Y = meet Y
set L = BoolePoset X;
let Y be non empty Subset of (BoolePoset X); ::_thesis: inf Y = meet Y
set y = the Element of Y;
A1: the carrier of (BoolePoset X) = bool X by LATTICE3:def_1;
then the Element of Y c= X ;
then reconsider Me = meet Y as Element of (BoolePoset X) by A1, SETFAM_1:7;
A2: now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_is_<=_than_Y_holds_
Me_>=_b
let b be Element of (BoolePoset X); ::_thesis: ( b is_<=_than Y implies Me >= b )
assume A3: b is_<=_than Y ; ::_thesis: Me >= b
now__::_thesis:_for_Z_being_set_st_Z_in_Y_holds_
b_c=_Z
let Z be set ; ::_thesis: ( Z in Y implies b c= Z )
assume A4: Z in Y ; ::_thesis: b c= Z
then reconsider Z9 = Z as Element of (BoolePoset X) ;
b <= Z9 by A3, A4, LATTICE3:def_8;
hence b c= Z by Th2; ::_thesis: verum
end;
then b c= Me by SETFAM_1:5;
hence Me >= b by Th2; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_in_Y_holds_
Me_<=_b
let b be Element of (BoolePoset X); ::_thesis: ( b in Y implies Me <= b )
assume b in Y ; ::_thesis: Me <= b
then Me c= b by SETFAM_1:3;
hence Me <= b by Th2; ::_thesis: verum
end;
then Me is_<=_than Y by LATTICE3:def_8;
hence inf Y = meet Y by A2, YELLOW_0:33; ::_thesis: verum
end;
theorem :: YELLOW_1:21
for X being set
for Y being Subset of (BoolePoset X) holds sup Y = union Y
proof
let X be set ; ::_thesis: for Y being Subset of (BoolePoset X) holds sup Y = union Y
set L = BoolePoset X;
let Y be Subset of (BoolePoset X); ::_thesis: sup Y = union Y
A1: the carrier of (BoolePoset X) = 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 (BoolePoset X) by A1, ZFMISC_1:81;
A2: now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_is_>=_than_Y_holds_
Un_<=_b
let b be Element of (BoolePoset X); ::_thesis: ( b is_>=_than Y implies Un <= b )
assume A3: b is_>=_than Y ; ::_thesis: Un <= b
now__::_thesis:_for_Z_being_set_st_Z_in_Y_holds_
Z_c=_b
let Z be set ; ::_thesis: ( Z in Y implies Z c= b )
assume A4: Z in Y ; ::_thesis: Z c= b
then reconsider Z9 = Z as Element of (BoolePoset X) ;
Z9 <= b by A3, A4, LATTICE3:def_9;
hence Z c= b by Th2; ::_thesis: verum
end;
then Un c= b by ZFMISC_1:76;
hence Un <= b by Th2; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(BoolePoset_X)_st_b_in_Y_holds_
b_<=_Un
let b be Element of (BoolePoset X); ::_thesis: ( b in Y implies b <= Un )
assume b in Y ; ::_thesis: b <= Un
then b c= Un by ZFMISC_1:74;
hence b <= Un by Th2; ::_thesis: verum
end;
then Un is_>=_than Y by LATTICE3:def_9;
hence sup Y = union Y by A2, YELLOW_0:30; ::_thesis: verum
end;
theorem :: YELLOW_1:22
for T being non empty TopSpace
for X being Subset of (InclPoset the topology of T) holds sup X = union X
proof
let T be non empty TopSpace; ::_thesis: for X being Subset of (InclPoset the topology of T) holds sup X = union X
set L = InclPoset the topology of T;
let X be Subset of (InclPoset the topology of T); ::_thesis: sup X = union X
reconsider X = X as Subset-Family of T by XBOOLE_1:1;
reconsider Un = union X as Element of (InclPoset the topology of T) by PRE_TOPC:def_1;
A1: now__::_thesis:_for_b_being_Element_of_(InclPoset_the_topology_of_T)_st_b_is_>=_than_X_holds_
Un_<=_b
let b be Element of (InclPoset the topology of T); ::_thesis: ( b is_>=_than X implies Un <= b )
assume A2: b is_>=_than X ; ::_thesis: Un <= b
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
Z_c=_b
let Z be set ; ::_thesis: ( Z in X implies Z c= b )
assume A3: Z in X ; ::_thesis: Z c= b
then reconsider Z9 = Z as Element of (InclPoset the topology of T) ;
Z9 <= b by A2, A3, LATTICE3:def_9;
hence Z c= b by Th3; ::_thesis: verum
end;
then Un c= b by ZFMISC_1:76;
hence Un <= b by Th3; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(InclPoset_the_topology_of_T)_st_b_in_X_holds_
b_<=_Un
let b be Element of (InclPoset the topology of T); ::_thesis: ( b in X implies b <= Un )
assume b in X ; ::_thesis: b <= Un
then b c= Un by ZFMISC_1:74;
hence b <= Un by Th3; ::_thesis: verum
end;
then Un is_>=_than X by LATTICE3:def_9;
hence sup X = union X by A1, YELLOW_0:30; ::_thesis: verum
end;
theorem :: YELLOW_1:23
for T being non empty TopSpace holds Bottom (InclPoset the topology of T) = {} by Th13, PRE_TOPC:1;
Lm2: for T being non empty TopSpace holds InclPoset the topology of T is lower-bounded
proof
let T be non empty TopSpace; ::_thesis: InclPoset the topology of T is lower-bounded
set L = InclPoset the topology of T;
reconsider x = {} as Element of (InclPoset the topology of T) by PRE_TOPC:1;
now__::_thesis:_ex_x_being_Element_of_(InclPoset_the_topology_of_T)_st_x_is_<=_than_the_carrier_of_(InclPoset_the_topology_of_T)
take x = x; ::_thesis: x is_<=_than the carrier of (InclPoset the topology of T)
thus x is_<=_than the carrier of (InclPoset the topology of T) ::_thesis: verum
proof
let b be Element of (InclPoset the topology of T); :: according to LATTICE3:def_8 ::_thesis: ( not b in the carrier of (InclPoset the topology of T) or x <= b )
assume b in the carrier of (InclPoset the topology of T) ; ::_thesis: x <= b
x c= b by XBOOLE_1:2;
hence x <= b by Th3; ::_thesis: verum
end;
end;
hence InclPoset the topology of T is lower-bounded by YELLOW_0:def_4; ::_thesis: verum
end;
theorem :: YELLOW_1:24
for T being non empty TopSpace holds Top (InclPoset the topology of T) = the carrier of T
proof
let T be non empty TopSpace; ::_thesis: Top (InclPoset the topology of T) = the carrier of T
set L = InclPoset the topology of T;
set C = the carrier of T;
the carrier of T = "/\" ({},(InclPoset the topology of T))
proof
reconsider C = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:def_1;
A1: for b being Element of (InclPoset the topology of T) st b is_<=_than {} holds
C >= b
proof
let b be Element of (InclPoset the topology of T); ::_thesis: ( b is_<=_than {} implies C >= b )
assume b is_<=_than {} ; ::_thesis: C >= b
b in the topology of T ;
hence C >= b by Th3; ::_thesis: verum
end;
C is_<=_than {} by YELLOW_0:6;
hence the carrier of T = "/\" ({},(InclPoset the topology of T)) by A1, YELLOW_0:31; ::_thesis: verum
end;
hence Top (InclPoset the topology of T) = the carrier of T by YELLOW_0:def_12; ::_thesis: verum
end;
Lm3: for T being non empty TopSpace holds InclPoset the topology of T is complete
proof
let T be non empty TopSpace; ::_thesis: InclPoset the topology of T is complete
set A = the topology of T;
reconsider IA = InclPoset the topology of T as lower-bounded Poset by Lm2;
for X being Subset of IA holds ex_sup_of X, InclPoset the topology of T
proof
let X be Subset of IA; ::_thesis: ex_sup_of X, InclPoset the topology of T
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 = union X as Element of (InclPoset the topology of T) by PRE_TOPC:def_1;
A1: for b being Element of (InclPoset the topology of T) st X is_<=_than b holds
N <= b
proof
let b be Element of (InclPoset the topology of T); ::_thesis: ( X is_<=_than b implies N <= b )
assume A2: X is_<=_than b ; ::_thesis: N <= b
now__::_thesis:_for_Z1_being_set_st_Z1_in_X_holds_
Z1_c=_b
let Z1 be set ; ::_thesis: ( Z1 in X implies Z1 c= b )
assume A3: Z1 in X ; ::_thesis: Z1 c= b
then reconsider Z19 = Z1 as Element of (InclPoset the topology of T) ;
Z19 <= b by A2, A3, LATTICE3:def_9;
hence Z1 c= b by Th3; ::_thesis: verum
end;
then union X c= b by ZFMISC_1:76;
hence N <= b by Th3; ::_thesis: verum
end;
X is_<=_than N
proof
let b be Element of (InclPoset the topology of T); :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= N )
assume b in X ; ::_thesis: b <= N
then b c= N by ZFMISC_1:74;
hence b <= N by Th3; ::_thesis: verum
end;
hence ex_sup_of X, InclPoset the topology of T by A1, YELLOW_0:15; ::_thesis: verum
end;
hence InclPoset the topology of T is complete by YELLOW_0:53; ::_thesis: verum
end;
Lm4: for T being non empty TopSpace holds not InclPoset the topology of T is trivial
proof
let T be non empty TopSpace; ::_thesis: not InclPoset the topology of T is trivial
set L = InclPoset the topology of T;
reconsider E = {} , S = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:1, PRE_TOPC:def_1;
E <> S ;
hence not InclPoset the topology of T is trivial by STRUCT_0:def_10; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster InclPoset the topology of T -> non trivial strict complete ;
coherence
( InclPoset the topology of T is complete & not InclPoset the topology of T is trivial ) by Lm3, Lm4;
end;
theorem :: YELLOW_1:25
for T being TopSpace
for 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; ::_thesis: for F being Subset-Family of T holds
( F is open iff F is Subset of (InclPoset the topology of T) )
let F be Subset-Family of T; ::_thesis: ( F is open iff F is Subset of (InclPoset the topology of T) )
hereby ::_thesis: ( F is Subset of (InclPoset the topology of T) implies F is open )
assume A1: F is open ; ::_thesis: F is Subset of (InclPoset the topology of T)
F c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in F or a in the topology of T )
assume A2: a in F ; ::_thesis: a in the topology of T
then reconsider a9 = a as Subset of T ;
a9 is open by A1, A2, TOPS_2:def_1;
hence a in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
hence F is Subset of (InclPoset the topology of T) ; ::_thesis: verum
end;
assume A3: F is Subset of (InclPoset the topology of T) ; ::_thesis: F is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
assume P in F ; ::_thesis: P is open
hence P is open by A3, PRE_TOPC:def_2; ::_thesis: verum
end;
begin
definition
let R be Relation;
attrR is RelStr-yielding means :Def3: :: YELLOW_1:def 3
for v being set st v in rng R holds
v is RelStr ;
end;
:: deftheorem Def3 defines RelStr-yielding YELLOW_1:def_3_:_
for R being Relation holds
( R is RelStr-yielding iff for v being set st v in rng R holds
v is RelStr );
registration
cluster Relation-like Function-like RelStr-yielding -> 1-sorted-yielding for set ;
coherence
for b1 being Function st b1 is RelStr-yielding holds
b1 is 1-sorted-yielding
proof
let F be Function; ::_thesis: ( F is RelStr-yielding implies F is 1-sorted-yielding )
assume A1: F is RelStr-yielding ; ::_thesis: F is 1-sorted-yielding
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in dom F or F . x is 1-sorted )
assume x in dom F ; ::_thesis: F . x is 1-sorted
then F . x in rng F by FUNCT_1:def_3;
hence F . x is 1-sorted by A1, Def3; ::_thesis: verum
end;
end;
registration
let I be set ;
cluster Relation-like I -defined Function-like V34(I) RelStr-yielding for set ;
existence
ex b1 being ManySortedSet of I st b1 is RelStr-yielding
proof
set R = the RelStr ;
take I --> the RelStr ; ::_thesis: I --> the RelStr is RelStr-yielding
let v be set ; :: according to YELLOW_1:def_3 ::_thesis: ( v in rng (I --> the RelStr ) implies v is RelStr )
assume A1: v in rng (I --> the RelStr ) ; ::_thesis: v is RelStr
rng (I --> the RelStr ) c= { the RelStr } by FUNCOP_1:13;
hence v is RelStr by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
definition
let J be non empty set ;
let A be RelStr-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine funcA . j -> RelStr ;
coherence
A . j is RelStr
proof
dom A = J by PARTFUN1:def_2;
then A . j in rng A by FUNCT_1:def_3;
hence A . j is RelStr by Def3; ::_thesis: verum
end;
end;
definition
let I be set ;
let J be RelStr-yielding ManySortedSet of I;
func product J -> strict RelStr means :Def4: :: YELLOW_1:def 4
( 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 being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) );
existence
ex b1 being strict RelStr st
( the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) )
proof
defpred S1[ set , set ] means ex f, g being Function st
( f = $1 & g = $2 & ( for i being set st i in I holds
ex R being RelStr ex 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 set holds
( [x,y] in R iff ( x in product (Carrier J) & y in product (Carrier J) & S1[x,y] ) ) from RELSET_1:sch_1();
take RS = RelStr(# (product (Carrier J)),R #); ::_thesis: ( the carrier of RS = product (Carrier J) & ( for x, y being Element of RS st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) )
thus the carrier of RS = product (Carrier J) ; ::_thesis: for x, y being Element of RS st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) )
let x, y be Element of RS; ::_thesis: ( x in product (Carrier J) implies ( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) )
assume A2: x in product (Carrier J) ; ::_thesis: ( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) )
hereby ::_thesis: ( ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) implies x <= y )
assume x <= y ; ::_thesis: ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex 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 ORDERS_2:def_5;
hence ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A1; ::_thesis: verum
end;
assume ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ; ::_thesis: x <= y
then [x,y] in the InternalRel of RS by A1, A2;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = product (Carrier J) & ( for x, y being Element of b1 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of b2 = product (Carrier J) & ( for x, y being Element of b2 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) holds
b1 = b2
proof
let S1, S2 be strict RelStr ; ::_thesis: ( the carrier of S1 = product (Carrier J) & ( 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 being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) & the carrier of S2 = product (Carrier J) & ( 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 being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) implies S1 = S2 )
assume 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 being set st i in I holds
ex R being RelStr ex 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 being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ; ::_thesis: S1 = S2
the InternalRel of S1 = the InternalRel of S2
proof
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of S1 or [a,b] in the InternalRel of S2 ) & ( not [a,b] in the InternalRel of S2 or [a,b] in the InternalRel of S1 ) )
hereby ::_thesis: ( not [a,b] in the InternalRel of S2 or [a,b] in the InternalRel of S1 )
assume A7: [a,b] in the InternalRel of S1 ; ::_thesis: [a,b] in the InternalRel of S2
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 being set st i in I holds
ex R being RelStr ex 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; ::_thesis: verum
end;
assume A9: [a,b] in the InternalRel of S2 ; ::_thesis: [a,b] in the InternalRel of S1
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 being set st i in I holds
ex R being RelStr ex 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 [a,b] in the InternalRel of S1 by ORDERS_2:def_5; ::_thesis: verum
end;
hence S1 = S2 by A3, A5; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines product YELLOW_1:def_4_:_
for I being set
for J being RelStr-yielding ManySortedSet of I
for b3 being strict RelStr holds
( b3 = product J iff ( the carrier of b3 = product (Carrier J) & ( for x, y being Element of b3 st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ) );
registration
let X be set ;
let L be RelStr ;
clusterX --> L -> RelStr-yielding ;
coherence
X --> L is RelStr-yielding
proof
let v be set ; :: according to YELLOW_1:def_3 ::_thesis: ( v in rng (X --> L) implies v is RelStr )
assume A1: v in rng (X --> L) ; ::_thesis: v is RelStr
rng (X --> L) c= {L} by FUNCOP_1:13;
hence v is RelStr by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
definition
let I be set ;
let T be RelStr ;
funcT |^ I -> strict RelStr equals :: YELLOW_1:def 5
product (I --> T);
correctness
coherence
product (I --> T) is strict RelStr ;
;
end;
:: deftheorem defines |^ YELLOW_1:def_5_:_
for I being set
for T being RelStr holds T |^ I = product (I --> T);
theorem Th26: :: YELLOW_1:26
for J being RelStr-yielding ManySortedSet of {} holds product J = RelStr(# {{}},(id {{}}) #)
proof
let J be RelStr-yielding ManySortedSet of {} ; ::_thesis: product J = RelStr(# {{}},(id {{}}) #)
set IT = product J;
A1: the carrier of (product J) = 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 (product J) by A1, TARSKI:def_1;
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of (product J) or [a,b] in id {{}} ) & ( not [a,b] in id {{}} or [a,b] in the InternalRel of (product J) ) )
x = {} --> {{}} ;
then reconsider f = x, g = y as Function ;
hereby ::_thesis: ( not [a,b] in id {{}} or [a,b] in the InternalRel of (product J) )
assume A3: [a,b] in the InternalRel of (product J) ; ::_thesis: [a,b] in id {{}}
then A4: b in the carrier of (product J) by ZFMISC_1:87;
A5: a in the carrier of (product J) 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; ::_thesis: verum
end;
assume A6: [a,b] in id {{}} ; ::_thesis: [a,b] in the InternalRel of (product J)
then a in {{}} by RELAT_1:def_10;
then A7: a = {} by TARSKI:def_1;
for i being set st i in {} holds
ex R being RelStr ex 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 [a,b] in the InternalRel of (product J) by A7, A8, ORDERS_2:def_5; ::_thesis: verum
end;
hence product J = RelStr(# {{}},(id {{}}) #) by A1; ::_thesis: verum
end;
theorem :: YELLOW_1:27
for Y being RelStr holds Y |^ {} = RelStr(# {{}},(id {{}}) #) by Th26;
theorem Th28: :: YELLOW_1:28
for X being set
for Y being RelStr holds Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
proof
let X be set ; ::_thesis: for Y being RelStr holds Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
let Y be RelStr ; ::_thesis: Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
set YY = the carrier of Y;
set f = Carrier (X --> Y);
A1: dom (Carrier (X --> Y)) = X by PARTFUN1:def_2;
A2: for x being set st x in X holds
(Carrier (X --> Y)) . x = the carrier of Y
proof
let x be set ; ::_thesis: ( x in X implies (Carrier (X --> Y)) . x = the carrier of Y )
assume A3: x in X ; ::_thesis: (Carrier (X --> Y)) . x = the carrier of Y
then ex R being 1-sorted st
( R = (X --> Y) . x & (Carrier (X --> Y)) . x = the carrier of R ) by PRALG_1:def_13;
hence (Carrier (X --> Y)) . x = the carrier of Y by A3, FUNCOP_1:7; ::_thesis: verum
end;
Funcs (X, the carrier of Y) = product (Carrier (X --> Y))
proof
thus Funcs (X, the carrier of Y) c= product (Carrier (X --> Y)) :: according to XBOOLE_0:def_10 ::_thesis: product (Carrier (X --> Y)) c= Funcs (X, the carrier of Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Funcs (X, the carrier of Y) or x in product (Carrier (X --> Y)) )
assume x in Funcs (X, the carrier of Y) ; ::_thesis: x in product (Carrier (X --> Y))
then consider g being Function such that
A4: x = g and
A5: dom g = X and
A6: rng g c= the carrier of Y by FUNCT_2:def_2;
now__::_thesis:_for_y_being_set_st_y_in_dom_(Carrier_(X_-->_Y))_holds_
g_._y_in_(Carrier_(X_-->_Y))_._y
let y be set ; ::_thesis: ( y in dom (Carrier (X --> Y)) implies g . y in (Carrier (X --> Y)) . y )
assume y in dom (Carrier (X --> Y)) ; ::_thesis: g . y in (Carrier (X --> Y)) . y
then ( (Carrier (X --> Y)) . y = the carrier of Y & g . y in rng g ) by A2, A5, FUNCT_1:def_3;
hence g . y in (Carrier (X --> Y)) . y by A6; ::_thesis: verum
end;
hence x in product (Carrier (X --> Y)) by A1, A4, A5, CARD_3:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Carrier (X --> Y)) or x in Funcs (X, the carrier of Y) )
assume x in product (Carrier (X --> Y)) ; ::_thesis: x in Funcs (X, the carrier of Y)
then consider g being Function such that
A7: x = g and
A8: dom g = dom (Carrier (X --> Y)) and
A9: for x being set st x in dom (Carrier (X --> Y)) holds
g . x in (Carrier (X --> Y)) . x by CARD_3:def_5;
rng g c= the carrier of Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in the carrier of Y )
assume y in rng g ; ::_thesis: y in the carrier of Y
then consider z being set such that
A10: z in dom g and
A11: y = g . z by FUNCT_1:def_3;
(Carrier (X --> Y)) . z = the carrier of Y by A2, A8, A10;
hence y in the carrier of Y by A8, A9, A10, A11; ::_thesis: verum
end;
hence x in Funcs (X, the carrier of Y) by A1, A7, A8, FUNCT_2:def_2; ::_thesis: verum
end;
hence Funcs (X, the carrier of Y) = the carrier of (Y |^ X) by Def4; ::_thesis: verum
end;
registration
let X be set ;
let Y be non empty RelStr ;
clusterY |^ X -> non empty strict ;
coherence
not Y |^ X is empty
proof
set f = the Function of X, the carrier of Y;
the Function of X, the carrier of Y in Funcs (X, the carrier of Y) by FUNCT_2:8;
hence not Y |^ X is empty by Th28; ::_thesis: verum
end;
end;
Lm5: for X being set
for Y being non empty RelStr
for x being 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 ; ::_thesis: for Y being non empty RelStr
for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
let Y be non empty RelStr ; ::_thesis: for x being Element of (Y |^ X) holds
( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
let x be Element of (Y |^ X); ::_thesis: ( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y )
x in the carrier of (Y |^ X) ;
then x in Funcs (X, the carrier of Y) by Th28;
hence ( x in the carrier of (product (X --> Y)) & x is Function of X, the carrier of Y ) by FUNCT_2:66; ::_thesis: verum
end;
registration
let X be set ;
let Y be non empty reflexive RelStr ;
clusterY |^ X -> strict reflexive ;
coherence
Y |^ X is reflexive
proof
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: Y |^ X is reflexive
hence Y |^ X is reflexive by Th26; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: Y |^ X is reflexive
then reconsider X = X as non empty set ;
for x being Element of (Y |^ X) holds x <= x
proof
let x be Element of (Y |^ X); ::_thesis: x <= 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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take x1 ; ::_thesis: ex g being Function st
( x1 = x9 & g = x9 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = g . i & xi <= yi ) ) )
take x1 ; ::_thesis: ( x1 = x9 & x1 = x9 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi ) ) )
thus ( x1 = x9 & x1 = x9 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi ) )
assume i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
then reconsider i = i as Element of X ;
take R = (X --> Y) . i; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
reconsider xi = x1 . i, yi = x1 . i as Element of R by FUNCOP_1:7;
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
reconsider xi1 = xi, yi1 = xi as Element of Y ;
xi1 <= yi1 ;
hence ( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi ) by FUNCOP_1:7; ::_thesis: verum
end;
x in the carrier of (product (X --> Y)) ;
then x9 in product (Carrier (X --> Y)) by Def4;
hence x <= x by A1, Def4; ::_thesis: verum
end;
hence Y |^ X is reflexive by YELLOW_0:def_1; ::_thesis: verum
end;
end;
end;
end;
registration
let Y be non empty RelStr ;
clusterY |^ {} -> 1 -element strict ;
coherence
Y |^ {} is 1 -element by Th26;
end;
registration
let Y be non empty reflexive RelStr ;
clusterY |^ {} -> strict antisymmetric with_suprema with_infima ;
coherence
( Y |^ {} is with_infima & Y |^ {} is with_suprema & Y |^ {} is antisymmetric ) ;
end;
registration
let X be set ;
let Y be non empty transitive RelStr ;
clusterY |^ X -> strict transitive ;
coherence
Y |^ X is transitive
proof
set IT = Y |^ X;
now__::_thesis:_for_x,_y,_z_being_Element_of_(Y_|^_X)_st_x_<=_y_&_y_<=_z_holds_
x_<=_z
let x, y, z be Element of (Y |^ X); ::_thesis: ( x <= y & y <= z implies x <= z )
reconsider x1 = x, y1 = y, z1 = z as Element of (product (X --> Y)) ;
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= 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 being set st i in X holds
ex R being RelStr ex 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 being set st i in X holds
ex R being RelStr ex 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 being set st i in X holds
ex R being RelStr ex 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 ; ::_thesis: ex g2 being Function st
( f2 = x1 & g2 = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )
take g2 ; ::_thesis: ( f2 = x1 & g2 = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )
thus ( f2 = x1 & g2 = z1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) )
assume A8: i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
then reconsider X = X as non empty set ;
reconsider i = i as Element of X by A8;
reconsider R = (X --> Y) . i as RelStr ;
A9: R = Y by FUNCOP_1:7;
then reconsider xi = f2 . i, yi = g2 . i as Element of R by FUNCT_2:5;
take R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f1 . i & yi2 = g1 . i & xi2 <= yi2 ) ) by A7, A4;
hence ( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) by A6, A3, A9, YELLOW_0:def_2; ::_thesis: verum
end;
hence x <= z by A5, Def4; ::_thesis: verum
end;
hence Y |^ X is transitive by YELLOW_0:def_2; ::_thesis: verum
end;
end;
registration
let X be set ;
let Y be non empty antisymmetric RelStr ;
clusterY |^ X -> strict antisymmetric ;
coherence
Y |^ X is antisymmetric
proof
set IT = Y |^ X;
now__::_thesis:_for_x,_y_being_Element_of_(Y_|^_X)_st_x_<=_y_&_y_<=_x_holds_
x_=_y
let x, y be Element of (Y |^ X); ::_thesis: ( x <= y & y <= x implies x = y )
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 ; ::_thesis: x = y
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 being set st i in X holds
ex R being RelStr ex 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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) by A1, Def4;
A7: now__::_thesis:_for_i_being_set_st_i_in_X_holds_
x19_._i_=_y19_._i
let i be set ; ::_thesis: ( i in X implies x19 . i = y19 . i )
assume A8: i in X ; ::_thesis: x19 . i = y19 . i
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; ::_thesis: verum
end;
( dom x19 = X & dom y19 = X ) by FUNCT_2:def_1;
hence x = y by A7, FUNCT_1:2; ::_thesis: verum
end;
hence Y |^ X is antisymmetric by YELLOW_0:def_3; ::_thesis: verum
end;
end;
registration
let X be non empty set ;
let Y be non empty antisymmetric with_infima RelStr ;
clusterY |^ X -> strict with_infima ;
coherence
Y |^ X is with_infima
proof
set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of (Y |^ X) st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of (Y |^ X) holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
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 S1[ set , set ] means ex xa, ya being Element of Y st
( xa = x9 . X & ya = y9 . X & Y = xa "/\" ya );
A1: for x being set st x in X holds
ex y being set st
( y in the carrier of Y & S1[x,y] )
proof
let a be set ; ::_thesis: ( a in X implies ex y being set st
( y in the carrier of Y & S1[a,y] ) )
assume a in X ; ::_thesis: ex y being set st
( y in the carrier of Y & S1[a,y] )
then reconsider xa = x9 . a, ya = y9 . a as Element of Y by FUNCT_2:5;
take y = xa "/\" ya; ::_thesis: ( y in the carrier of Y & S1[a,y] )
thus y in the carrier of Y ; ::_thesis: S1[a,y]
take xa ; ::_thesis: ex ya being Element of Y st
( xa = x9 . a & ya = y9 . a & y = xa "/\" ya )
take ya ; ::_thesis: ( xa = x9 . a & ya = y9 . a & y = xa "/\" ya )
thus ( xa = x9 . a & ya = y9 . a & y = xa "/\" ya ) ; ::_thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A2: for a being set st a in X holds
S1[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 (Y |^ X) by Th28;
take z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of (Y |^ X) holds
( not b1 <= x or not b1 <= y or b1 <= 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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take f ; ::_thesis: ex g being Function st
( f = z1 & g = y1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take y9 ; ::_thesis: ( f = z1 & y9 = y1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) ) )
thus ( f = z1 & y9 = y1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) )
assume i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = f . i, yi = y9 . i as Element of R by FUNCOP_1:7;
take R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2, FUNCOP_1:7;
hence ( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) by YELLOW_0:23; ::_thesis: verum
end;
z1 in the carrier of (product (X --> Y)) ;
then z1 in product (Carrier (X --> Y)) by Def4;
hence z <= y by A4, Def4; ::_thesis: verum
end;
A5: for z9 being Element of (Y |^ X) st z9 <= x & z9 <= y holds
z9 <= z
proof
let z9 be Element of (Y |^ X); ::_thesis: ( z9 <= x & z9 <= y implies z9 <= z )
assume that
A6: z9 <= x and
A7: z9 <= y ; ::_thesis: z9 <= z
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 being set st i in X holds
ex R being RelStr ex 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 being set st i in X holds
ex R being RelStr ex 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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take J ; ::_thesis: ex g being Function st
( J = z2 & g = z3 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = g . i & xi <= yi ) ) )
take K ; ::_thesis: ( J = z2 & K = z3 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) ) )
thus ( J = z2 & K = z3 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) )
assume i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = J . i, yi = K . i as Element of R by FUNCOP_1:7;
take R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
A13: ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2, FUNCOP_1:7;
( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f1 . i & yi1 = g1 . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f2 . i & yi2 = g2 . i & xi2 <= yi2 ) ) by A10, A12;
hence ( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) by A9, A11, A13, YELLOW_0:23; ::_thesis: verum
end;
hence z9 <= z by A8, Def4; ::_thesis: verum
end;
hence z9 <= z ; ::_thesis: verum
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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take f ; ::_thesis: ex g being Function st
( f = z1 & g = x1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take x9 ; ::_thesis: ( f = z1 & x9 = x1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) ) )
thus ( f = z1 & x9 = x1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) )
assume i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = f . i, yi = x9 . i as Element of R by FUNCOP_1:7;
take R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2, FUNCOP_1:7;
hence ( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) by YELLOW_0:23; ::_thesis: verum
end;
z1 in the carrier of (product (X --> Y)) ;
then z1 in product (Carrier (X --> Y)) by Def4;
hence z <= x by A14, Def4; ::_thesis: verum
end;
hence ( z <= x & z <= y & ( for b1 being Element of the carrier of (Y |^ X) holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) ) by A3, A5; ::_thesis: verum
end;
end;
registration
let X be non empty set ;
let Y be non empty antisymmetric with_suprema RelStr ;
clusterY |^ X -> strict with_suprema ;
coherence
Y |^ X is with_suprema
proof
set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of (Y |^ X) st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of (Y |^ X) holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
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 S1[ set , set ] means ex xa, ya being Element of Y st
( xa = x9 . X & ya = y9 . X & Y = xa "\/" ya );
A1: for x being set st x in X holds
ex y being set st
( y in the carrier of Y & S1[x,y] )
proof
let a be set ; ::_thesis: ( a in X implies ex y being set st
( y in the carrier of Y & S1[a,y] ) )
assume a in X ; ::_thesis: ex y being set st
( y in the carrier of Y & S1[a,y] )
then reconsider xa = x9 . a, ya = y9 . a as Element of Y by FUNCT_2:5;
take y = xa "\/" ya; ::_thesis: ( y in the carrier of Y & S1[a,y] )
thus y in the carrier of Y ; ::_thesis: S1[a,y]
take xa ; ::_thesis: ex ya being Element of Y st
( xa = x9 . a & ya = y9 . a & y = xa "\/" ya )
take ya ; ::_thesis: ( xa = x9 . a & ya = y9 . a & y = xa "\/" ya )
thus ( xa = x9 . a & ya = y9 . a & y = xa "\/" ya ) ; ::_thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A2: for a being set st a in X holds
S1[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 (Y |^ X) by Th28;
take z ; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of (Y |^ X) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take y9 ; ::_thesis: ex g being Function st
( y9 = y1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = g . i & xi <= yi ) ) )
take f ; ::_thesis: ( y9 = y1 & f = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) ) )
thus ( y9 = y1 & f = z1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) )
assume i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = f . i, xi = y9 . i as Element of R by FUNCOP_1:7;
take R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:7;
hence ( R = (X --> Y) . i & xi = y9 . i & yi = f . i & xi <= yi ) by YELLOW_0:22; ::_thesis: verum
end;
y1 in the carrier of (product (X --> Y)) ;
then y1 in product (Carrier (X --> Y)) by Def4;
hence y <= z by A4, Def4; ::_thesis: verum
end;
A5: for z9 being Element of (Y |^ X) st z9 >= x & z9 >= y holds
z9 >= z
proof
let z9 be Element of (Y |^ X); ::_thesis: ( z9 >= x & z9 >= y implies z9 >= z )
assume that
A6: z9 >= x and
A7: z9 >= y ; ::_thesis: z9 >= z
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 being set st i in X holds
ex R being RelStr ex 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 being set st i in X holds
ex R being RelStr ex 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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take K ; ::_thesis: ex g being Function st
( K = z3 & g = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = g . i & xi <= yi ) ) )
take J ; ::_thesis: ( K = z3 & J = z2 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) ) )
thus ( K = z3 & J = z2 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) )
assume i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = J . i, xi = K . i as Element of R by FUNCOP_1:7;
take R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi )
A13: ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:7;
( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f1 . i & yi1 = g1 . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f2 . i & yi2 = g2 . i & xi2 <= yi2 ) ) by A11, A9;
hence ( R = (X --> Y) . i & xi = K . i & yi = J . i & xi <= yi ) by A10, A8, A13, YELLOW_0:22; ::_thesis: verum
end;
z3 in the carrier of (product (X --> Y)) ;
then z3 in product (Carrier (X --> Y)) by Def4;
hence z9 >= z by A12, Def4; ::_thesis: verum
end;
hence z9 >= z ; ::_thesis: verum
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 being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take x9 ; ::_thesis: ex g being Function st
( x9 = x1 & g = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = g . i & xi <= yi ) ) )
take f ; ::_thesis: ( x9 = x1 & f = z1 & ( for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) ) )
thus ( x9 = x1 & f = z1 ) ; ::_thesis: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) )
assume i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider yi = f . i, xi = x9 . i as Element of R by FUNCOP_1:7;
take R ; ::_thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
take xi ; ::_thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
take yi ; ::_thesis: ( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "\/" ya ) ) by A2, FUNCOP_1:7;
hence ( R = (X --> Y) . i & xi = x9 . i & yi = f . i & xi <= yi ) by YELLOW_0:22; ::_thesis: verum
end;
x1 in the carrier of (product (X --> Y)) ;
then x1 in product (Carrier (X --> Y)) by Def4;
hence x <= z by A14, Def4; ::_thesis: verum
end;
hence ( x <= z & y <= z & ( for b1 being Element of the carrier of (Y |^ X) holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) ) by A3, A5; ::_thesis: verum
end;
end;
definition
let S, T be RelStr ;
func MonMaps (S,T) -> strict full SubRelStr of T |^ the carrier of S means :: YELLOW_1:def 6
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
ex b1 being strict full SubRelStr of T |^ the carrier of S st
for f being Function of S,T holds
( f in the carrier of b1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )
proof
set X = MonFuncs (S,T);
MonFuncs (S,T) c= Funcs ( the carrier of S, the carrier of T) by ORDERS_3:11;
then reconsider X = MonFuncs (S,T) as Subset of (T |^ the carrier of S) by Th28;
take SX = subrelstr X; ::_thesis: for f being Function of S,T holds
( f in the carrier of SX iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )
let f be Function of S,T; ::_thesis: ( f in the carrier of SX iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) )
hereby ::_thesis: ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone implies f in the carrier of SX )
assume f in the carrier of SX ; ::_thesis: ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone )
then f in X by YELLOW_0:def_15;
then ex f9 being 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 ) ; ::_thesis: verum
end;
assume ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ; ::_thesis: f in the carrier of SX
then f in X by ORDERS_3:def_6;
hence f in the carrier of SX by YELLOW_0:def_15; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict full SubRelStr of T |^ the carrier of S st ( for f being Function of S,T holds
( f in the carrier of b1 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) & ( for f being Function of S,T holds
( f in the carrier of b2 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) ) holds
b1 = b2
proof
let A1, A2 be strict full SubRelStr of T |^ the carrier of S; ::_thesis: ( ( 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 ) ) ) & ( 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 ) ) ) implies A1 = A2 )
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 ) ) ; ::_thesis: A1 = A2
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of A2 or a in the carrier of A1 )
assume A5: a in the carrier of A2 ; ::_thesis: a in the carrier of A1
then reconsider f = a as Function of S,T by A3, FUNCT_2:66;
f is monotone by A2, A5;
hence a in the carrier of A1 by A1, A3, A5; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of A1 or a in the carrier of A2 )
assume A7: a in the carrier of A1 ; ::_thesis: a in the carrier of A2
then reconsider f = a as Function of S,T by A6, FUNCT_2:66;
f is monotone by A1, A7;
hence a in the carrier of A2 by A2, A6, A7; ::_thesis: verum
end;
then the carrier of A1 = the carrier of A2 by A4, XBOOLE_0:def_10;
hence A1 = A2 by YELLOW_0:57; ::_thesis: verum
end;
end;
:: deftheorem defines MonMaps YELLOW_1:def_6_:_
for S, T being RelStr
for b3 being strict full SubRelStr of T |^ the carrier of S holds
( b3 = MonMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b3 iff ( f in Funcs ( the carrier of S, the carrier of T) & f is monotone ) ) );