:: WAYBEL20 semantic presentation
begin
theorem Th1: :: WAYBEL20:1
for X being set
for S being Subset of (id X) holds proj1 S = proj2 S
proof
let X be set ; ::_thesis: for S being Subset of (id X) holds proj1 S = proj2 S
let S be Subset of (id X); ::_thesis: proj1 S = proj2 S
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_proj1_S_implies_x_in_proj2_S_)_&_(_x_in_proj2_S_implies_x_in_proj1_S_)_)
let x be set ; ::_thesis: ( ( x in proj1 S implies x in proj2 S ) & ( x in proj2 S implies x in proj1 S ) )
hereby ::_thesis: ( x in proj2 S implies x in proj1 S )
assume x in proj1 S ; ::_thesis: x in proj2 S
then consider y being set such that
A1: [x,y] in S by XTUPLE_0:def_12;
x = y by A1, RELAT_1:def_10;
hence x in proj2 S by A1, XTUPLE_0:def_13; ::_thesis: verum
end;
assume x in proj2 S ; ::_thesis: x in proj1 S
then consider y being set such that
A2: [y,x] in S by XTUPLE_0:def_13;
x = y by A2, RELAT_1:def_10;
hence x in proj1 S by A2, XTUPLE_0:def_12; ::_thesis: verum
end;
hence proj1 S = proj2 S by TARSKI:1; ::_thesis: verum
end;
theorem Th2: :: WAYBEL20:2
for X, Y being non empty set
for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X
proof
let X, Y be non empty set ; ::_thesis: for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X
let f be Function of X,Y; ::_thesis: [:f,f:] " (id Y) is Equivalence_Relation of X
set ff = [:f,f:] " (id Y);
A1: dom f = X by FUNCT_2:def_1;
reconsider R9 = [:f,f:] " (id Y) as Relation of X ;
A2: dom [:f,f:] = [:(dom f),(dom f):] by FUNCT_3:def_8;
R9 is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in R9 )
assume A3: x in X ; ::_thesis: [x,x] in R9
then reconsider x9 = x as Element of X ;
A4: [(f . x9),(f . x9)] in id Y by RELAT_1:def_10;
( [x,x] in dom [:f,f:] & [(f . x),(f . x)] = [:f,f:] . (x,x) ) by A2, A1, A3, FUNCT_3:def_8, ZFMISC_1:def_2;
hence [x,x] in R9 by A4, FUNCT_1:def_7; ::_thesis: verum
end;
then A5: ( dom R9 = X & field R9 = X ) by ORDERS_1:13;
A6: R9 is_symmetric_in X
proof
let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in X or not y in X or not [x,y] in R9 or [y,x] in R9 )
assume that
A7: ( x in X & y in X ) and
A8: [x,y] in R9 ; ::_thesis: [y,x] in R9
reconsider x9 = x, y9 = y as Element of X by A7;
A9: ( [y,x] in dom [:f,f:] & [(f . y),(f . x)] = [:f,f:] . (y,x) ) by A2, A1, A7, FUNCT_3:def_8, ZFMISC_1:def_2;
A10: ( [:f,f:] . [x,y] in id Y & [(f . x),(f . y)] = [:f,f:] . (x,y) ) by A1, A7, A8, FUNCT_1:def_7, FUNCT_3:def_8;
then f . x9 = f . y9 by RELAT_1:def_10;
hence [y,x] in R9 by A10, A9, FUNCT_1:def_7; ::_thesis: verum
end;
R9 is_transitive_in X
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in R9 or not [y,z] in R9 or [x,z] in R9 )
assume that
A11: x in X and
A12: y in X and
A13: z in X and
A14: [x,y] in R9 and
A15: [y,z] in R9 ; ::_thesis: [x,z] in R9
A16: ( [x,z] in dom [:f,f:] & [(f . x),(f . z)] = [:f,f:] . (x,z) ) by A2, A1, A11, A13, FUNCT_3:def_8, ZFMISC_1:def_2;
reconsider y9 = y, z9 = z as Element of X by A12, A13;
( [:f,f:] . [y,z] in id Y & [(f . y),(f . z)] = [:f,f:] . (y,z) ) by A1, A12, A13, A15, FUNCT_1:def_7, FUNCT_3:def_8;
then A17: f . y9 = f . z9 by RELAT_1:def_10;
( [:f,f:] . [x,y] in id Y & [(f . x),(f . y)] = [:f,f:] . (x,y) ) by A1, A11, A12, A14, FUNCT_1:def_7, FUNCT_3:def_8;
hence [x,z] in R9 by A17, A16, FUNCT_1:def_7; ::_thesis: verum
end;
hence [:f,f:] " (id Y) is Equivalence_Relation of X by A5, A6, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;
definition
let L1, L2, T1, T2 be RelStr ;
let f be Function of L1,T1;
let g be Function of L2,T2;
:: original: [:
redefine func[:f,g:] -> Function of [:L1,L2:],[:T1,T2:];
coherence
[:f,g:] is Function of [:L1,L2:],[:T1,T2:]
proof
( the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] & the carrier of [:T1,T2:] = [: the carrier of T1, the carrier of T2:] ) by YELLOW_3:def_2;
hence [:f,g:] is Function of [:L1,L2:],[:T1,T2:] ; ::_thesis: verum
end;
end;
theorem Th3: :: WAYBEL20:3
for f, g being Function
for X being set holds
( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) )
proof
let f, g be Function; ::_thesis: for X being set holds
( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) )
let X be set ; ::_thesis: ( proj1 ([:f,g:] .: X) c= f .: (proj1 X) & proj2 ([:f,g:] .: X) c= g .: (proj2 X) )
A1: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8;
hereby :: according to TARSKI:def_3 ::_thesis: proj2 ([:f,g:] .: X) c= g .: (proj2 X)
let x be set ; ::_thesis: ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) )
assume x in proj1 ([:f,g:] .: X) ; ::_thesis: x in f .: (proj1 X)
then consider y being set such that
A2: [x,y] in [:f,g:] .: X by XTUPLE_0:def_12;
consider xy being set such that
A3: xy in dom [:f,g:] and
A4: xy in X and
A5: [x,y] = [:f,g:] . xy by A2, FUNCT_1:def_6;
consider x9, y9 being set such that
A6: x9 in dom f and
A7: y9 in dom g and
A8: xy = [x9,y9] by A1, A3, ZFMISC_1:def_2;
[x,y] = [:f,g:] . (x9,y9) by A5, A8
.= [(f . x9),(g . y9)] by A6, A7, FUNCT_3:def_8 ;
then A9: x = f . x9 by XTUPLE_0:1;
x9 in proj1 X by A4, A8, XTUPLE_0:def_12;
hence x in f .: (proj1 X) by A6, A9, FUNCT_1:def_6; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 ([:f,g:] .: X) or y in g .: (proj2 X) )
assume y in proj2 ([:f,g:] .: X) ; ::_thesis: y in g .: (proj2 X)
then consider x being set such that
A10: [x,y] in [:f,g:] .: X by XTUPLE_0:def_13;
consider xy being set such that
A11: xy in dom [:f,g:] and
A12: xy in X and
A13: [x,y] = [:f,g:] . xy by A10, FUNCT_1:def_6;
consider x9, y9 being set such that
A14: x9 in dom f and
A15: y9 in dom g and
A16: xy = [x9,y9] by A1, A11, ZFMISC_1:def_2;
[x,y] = [:f,g:] . (x9,y9) by A13, A16
.= [(f . x9),(g . y9)] by A14, A15, FUNCT_3:def_8 ;
then A17: y = g . y9 by XTUPLE_0:1;
y9 in proj2 X by A12, A16, XTUPLE_0:def_13;
hence y in g .: (proj2 X) by A15, A17, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th4: :: WAYBEL20:4
for f, g being Function
for X being set st X c= [:(dom f),(dom g):] holds
( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) )
proof
let f, g be Function; ::_thesis: for X being set st X c= [:(dom f),(dom g):] holds
( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) )
let X be set ; ::_thesis: ( X c= [:(dom f),(dom g):] implies ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) ) )
assume A1: X c= [:(dom f),(dom g):] ; ::_thesis: ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) )
A2: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def_8;
A3: proj1 ([:f,g:] .: X) c= f .: (proj1 X) by Th3;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_proj1_([:f,g:]_.:_X)_implies_x_in_f_.:_(proj1_X)_)_&_(_x_in_f_.:_(proj1_X)_implies_x_in_proj1_([:f,g:]_.:_X)_)_)
let x be set ; ::_thesis: ( ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) & ( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) ) )
thus ( x in proj1 ([:f,g:] .: X) implies x in f .: (proj1 X) ) by A3; ::_thesis: ( x in f .: (proj1 X) implies x in proj1 ([:f,g:] .: X) )
assume x in f .: (proj1 X) ; ::_thesis: x in proj1 ([:f,g:] .: X)
then consider x9 being set such that
A4: x9 in dom f and
A5: x9 in proj1 X and
A6: x = f . x9 by FUNCT_1:def_6;
consider y9 being set such that
A7: [x9,y9] in X by A5, XTUPLE_0:def_12;
y9 in dom g by A1, A7, ZFMISC_1:87;
then [:f,g:] . (x9,y9) = [(f . x9),(g . y9)] by A4, FUNCT_3:def_8;
then [x,(g . y9)] in [:f,g:] .: X by A1, A2, A6, A7, FUNCT_1:def_6;
hence x in proj1 ([:f,g:] .: X) by XTUPLE_0:def_12; ::_thesis: verum
end;
hence proj1 ([:f,g:] .: X) = f .: (proj1 X) by TARSKI:1; ::_thesis: proj2 ([:f,g:] .: X) = g .: (proj2 X)
A8: proj2 ([:f,g:] .: X) c= g .: (proj2 X) by Th3;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_proj2_([:f,g:]_.:_X)_implies_x_in_g_.:_(proj2_X)_)_&_(_x_in_g_.:_(proj2_X)_implies_x_in_proj2_([:f,g:]_.:_X)_)_)
let x be set ; ::_thesis: ( ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) & ( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) ) )
thus ( x in proj2 ([:f,g:] .: X) implies x in g .: (proj2 X) ) by A8; ::_thesis: ( x in g .: (proj2 X) implies x in proj2 ([:f,g:] .: X) )
assume x in g .: (proj2 X) ; ::_thesis: x in proj2 ([:f,g:] .: X)
then consider x9 being set such that
A9: x9 in dom g and
A10: x9 in proj2 X and
A11: x = g . x9 by FUNCT_1:def_6;
consider y9 being set such that
A12: [y9,x9] in X by A10, XTUPLE_0:def_13;
y9 in dom f by A1, A12, ZFMISC_1:87;
then [:f,g:] . (y9,x9) = [(f . y9),(g . x9)] by A9, FUNCT_3:def_8;
then [(f . y9),x] in [:f,g:] .: X by A1, A2, A11, A12, FUNCT_1:def_6;
hence x in proj2 ([:f,g:] .: X) by XTUPLE_0:def_13; ::_thesis: verum
end;
hence proj2 ([:f,g:] .: X) = g .: (proj2 X) by TARSKI:1; ::_thesis: verum
end;
theorem Th5: :: WAYBEL20:5
for S being non empty antisymmetric RelStr st ex_inf_of {} ,S holds
S is upper-bounded
proof
let S be non empty antisymmetric RelStr ; ::_thesis: ( ex_inf_of {} ,S implies S is upper-bounded )
assume A1: ex_inf_of {} ,S ; ::_thesis: S is upper-bounded
take Top S ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of S is_<=_than Top S
let x be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not x in the carrier of S or x <= Top S )
{} is_>=_than x by YELLOW_0:6;
hence ( not x in the carrier of S or x <= Top S ) by A1, YELLOW_0:31; ::_thesis: verum
end;
theorem Th6: :: WAYBEL20:6
for S being non empty antisymmetric RelStr st ex_sup_of {} ,S holds
S is lower-bounded
proof
let S be non empty antisymmetric RelStr ; ::_thesis: ( ex_sup_of {} ,S implies S is lower-bounded )
assume A1: ex_sup_of {} ,S ; ::_thesis: S is lower-bounded
take Bottom S ; :: according to YELLOW_0:def_4 ::_thesis: Bottom S is_<=_than the carrier of S
let x be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not x in the carrier of S or Bottom S <= x )
{} is_<=_than x by YELLOW_0:6;
hence ( not x in the carrier of S or Bottom S <= x ) by A1, YELLOW_0:30; ::_thesis: verum
end;
theorem Th7: :: WAYBEL20:7
for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
proof
let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
let D be Subset of [:L1,L2:]; ::_thesis: ( ex_inf_of D,[:L1,L2:] implies inf D = [(inf (proj1 D)),(inf (proj2 D))] )
assume A1: ex_inf_of D,[:L1,L2:] ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
percases ( D <> {} or D = {} ) ;
suppose D <> {} ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A1, YELLOW_3:47; ::_thesis: verum
end;
supposeA2: D = {} ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
then ex_inf_of {} ,L2 by A1, FUNCT_5:8, YELLOW_3:42;
then A3: L2 is upper-bounded by Th5;
ex_inf_of {} ,L1 by A1, A2, FUNCT_5:8, YELLOW_3:42;
then L1 is upper-bounded by Th5;
hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A1, A3, YELLOW10:6; ::_thesis: verum
end;
end;
end;
theorem Th8: :: WAYBEL20:8
for L1, L2 being non empty antisymmetric RelStr
for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
proof
let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
let D be Subset of [:L1,L2:]; ::_thesis: ( ex_sup_of D,[:L1,L2:] implies sup D = [(sup (proj1 D)),(sup (proj2 D))] )
assume A1: ex_sup_of D,[:L1,L2:] ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
percases ( D <> {} or D = {} ) ;
suppose D <> {} ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A1, YELLOW_3:46; ::_thesis: verum
end;
supposeA2: D = {} ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
then ex_sup_of {} ,L2 by A1, FUNCT_5:8, YELLOW_3:41;
then A3: L2 is lower-bounded by Th6;
ex_sup_of {} ,L1 by A1, A2, FUNCT_5:8, YELLOW_3:41;
then L1 is lower-bounded by Th6;
hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A1, A3, YELLOW10:5; ::_thesis: verum
end;
end;
end;
theorem Th9: :: WAYBEL20:9
for L1, L2, T1, T2 being non empty antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds
[:f,g:] is infs-preserving
proof
let L1, L2, T1, T2 be non empty antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1
for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds
[:f,g:] is infs-preserving
let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is infs-preserving & g is infs-preserving holds
[:f,g:] is infs-preserving
let g be Function of L2,T2; ::_thesis: ( f is infs-preserving & g is infs-preserving implies [:f,g:] is infs-preserving )
assume that
A1: f is infs-preserving and
A2: g is infs-preserving ; ::_thesis: [:f,g:] is infs-preserving
let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_32 ::_thesis: [:f,g:] preserves_inf_of X
A3: f preserves_inf_of proj1 X by A1, WAYBEL_0:def_32;
A4: g preserves_inf_of proj2 X by A2, WAYBEL_0:def_32;
set iX = [:f,g:] .: X;
A5: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1;
assume A6: ex_inf_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of [:f,g:] .: X,[:T1,T2:] & "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:])) )
then A7: ex_inf_of proj1 X,L1 by YELLOW_3:42;
A8: ex_inf_of proj2 X,L2 by A6, YELLOW_3:42;
X c= the carrier of [:L1,L2:] ;
then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2;
then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A5, Th4;
then A11: ex_inf_of proj2 ([:f,g:] .: X),T2 by A4, A8, WAYBEL_0:def_30;
A12: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A5, A9, Th4;
then ex_inf_of proj1 ([:f,g:] .: X),T1 by A3, A7, WAYBEL_0:def_30;
hence ex_inf_of [:f,g:] .: X,[:T1,T2:] by A11, YELLOW_3:42; ::_thesis: "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:]))
hence inf ([:f,g:] .: X) = [(inf (f .: (proj1 X))),(inf (g .: (proj2 X)))] by A12, A10, Th7
.= [(f . (inf (proj1 X))),(inf (g .: (proj2 X)))] by A3, A7, WAYBEL_0:def_30
.= [(f . (inf (proj1 X))),(g . (inf (proj2 X)))] by A4, A8, WAYBEL_0:def_30
.= [:f,g:] . ((inf (proj1 X)),(inf (proj2 X))) by A5, FUNCT_3:def_8
.= [:f,g:] . (inf X) by A6, Th7 ;
::_thesis: verum
end;
theorem :: WAYBEL20:10
for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving
proof
let L1, L2, T1, T2 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1
for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving
let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving
let g be Function of L2,T2; ::_thesis: ( f is filtered-infs-preserving & g is filtered-infs-preserving implies [:f,g:] is filtered-infs-preserving )
assume that
A1: f is filtered-infs-preserving and
A2: g is filtered-infs-preserving ; ::_thesis: [:f,g:] is filtered-infs-preserving
let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or [:f,g:] preserves_inf_of X )
assume A3: ( not X is empty & X is filtered ) ; ::_thesis: [:f,g:] preserves_inf_of X
then ( not proj1 X is empty & proj1 X is filtered ) by YELLOW_3:21, YELLOW_3:24;
then A4: f preserves_inf_of proj1 X by A1, WAYBEL_0:def_36;
( not proj2 X is empty & proj2 X is filtered ) by A3, YELLOW_3:21, YELLOW_3:24;
then A5: g preserves_inf_of proj2 X by A2, WAYBEL_0:def_36;
set iX = [:f,g:] .: X;
A6: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1;
assume A7: ex_inf_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of [:f,g:] .: X,[:T1,T2:] & "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:])) )
then A8: ex_inf_of proj1 X,L1 by YELLOW_3:42;
X c= the carrier of [:L1,L2:] ;
then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2;
then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A6, Th4;
A11: ex_inf_of proj2 X,L2 by A7, YELLOW_3:42;
then A12: ex_inf_of proj2 ([:f,g:] .: X),T2 by A5, A10, WAYBEL_0:def_30;
A13: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A6, A9, Th4;
then ex_inf_of proj1 ([:f,g:] .: X),T1 by A4, A8, WAYBEL_0:def_30;
hence ex_inf_of [:f,g:] .: X,[:T1,T2:] by A12, YELLOW_3:42; ::_thesis: "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:]))
hence inf ([:f,g:] .: X) = [(inf (f .: (proj1 X))),(inf (g .: (proj2 X)))] by A13, A10, Th7
.= [(f . (inf (proj1 X))),(inf (g .: (proj2 X)))] by A4, A8, WAYBEL_0:def_30
.= [(f . (inf (proj1 X))),(g . (inf (proj2 X)))] by A5, A11, WAYBEL_0:def_30
.= [:f,g:] . ((inf (proj1 X)),(inf (proj2 X))) by A6, FUNCT_3:def_8
.= [:f,g:] . (inf X) by A7, Th7 ;
::_thesis: verum
end;
theorem :: WAYBEL20:11
for L1, L2, T1, T2 being non empty antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds
[:f,g:] is sups-preserving
proof
let L1, L2, T1, T2 be non empty antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1
for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds
[:f,g:] is sups-preserving
let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is sups-preserving & g is sups-preserving holds
[:f,g:] is sups-preserving
let g be Function of L2,T2; ::_thesis: ( f is sups-preserving & g is sups-preserving implies [:f,g:] is sups-preserving )
assume that
A1: f is sups-preserving and
A2: g is sups-preserving ; ::_thesis: [:f,g:] is sups-preserving
let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_33 ::_thesis: [:f,g:] preserves_sup_of X
A3: f preserves_sup_of proj1 X by A1, WAYBEL_0:def_33;
A4: g preserves_sup_of proj2 X by A2, WAYBEL_0:def_33;
set iX = [:f,g:] .: X;
A5: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1;
assume A6: ex_sup_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of [:f,g:] .: X,[:T1,T2:] & "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:])) )
then A7: ex_sup_of proj1 X,L1 by YELLOW_3:41;
A8: ex_sup_of proj2 X,L2 by A6, YELLOW_3:41;
X c= the carrier of [:L1,L2:] ;
then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2;
then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A5, Th4;
then A11: ex_sup_of proj2 ([:f,g:] .: X),T2 by A4, A8, WAYBEL_0:def_31;
A12: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A5, A9, Th4;
then ex_sup_of proj1 ([:f,g:] .: X),T1 by A3, A7, WAYBEL_0:def_31;
hence ex_sup_of [:f,g:] .: X,[:T1,T2:] by A11, YELLOW_3:41; ::_thesis: "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:]))
hence sup ([:f,g:] .: X) = [(sup (f .: (proj1 X))),(sup (g .: (proj2 X)))] by A12, A10, Th8
.= [(f . (sup (proj1 X))),(sup (g .: (proj2 X)))] by A3, A7, WAYBEL_0:def_31
.= [(f . (sup (proj1 X))),(g . (sup (proj2 X)))] by A4, A8, WAYBEL_0:def_31
.= [:f,g:] . ((sup (proj1 X)),(sup (proj2 X))) by A5, FUNCT_3:def_8
.= [:f,g:] . (sup X) by A6, Th8 ;
::_thesis: verum
end;
theorem Th12: :: WAYBEL20:12
for L1, L2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of L1,T1
for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds
[:f,g:] is directed-sups-preserving
proof
let L1, L2, T1, T2 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,T1
for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds
[:f,g:] is directed-sups-preserving
let f be Function of L1,T1; ::_thesis: for g being Function of L2,T2 st f is directed-sups-preserving & g is directed-sups-preserving holds
[:f,g:] is directed-sups-preserving
let g be Function of L2,T2; ::_thesis: ( f is directed-sups-preserving & g is directed-sups-preserving implies [:f,g:] is directed-sups-preserving )
assume that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving ; ::_thesis: [:f,g:] is directed-sups-preserving
let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or [:f,g:] preserves_sup_of X )
assume A3: ( not X is empty & X is directed ) ; ::_thesis: [:f,g:] preserves_sup_of X
then ( not proj1 X is empty & proj1 X is directed ) by YELLOW_3:21, YELLOW_3:22;
then A4: f preserves_sup_of proj1 X by A1, WAYBEL_0:def_37;
( not proj2 X is empty & proj2 X is directed ) by A3, YELLOW_3:21, YELLOW_3:22;
then A5: g preserves_sup_of proj2 X by A2, WAYBEL_0:def_37;
set iX = [:f,g:] .: X;
A6: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def_1;
assume A7: ex_sup_of X,[:L1,L2:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of [:f,g:] .: X,[:T1,T2:] & "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:])) )
then A8: ex_sup_of proj1 X,L1 by YELLOW_3:41;
X c= the carrier of [:L1,L2:] ;
then A9: X c= [: the carrier of L1, the carrier of L2:] by YELLOW_3:def_2;
then A10: proj2 ([:f,g:] .: X) = g .: (proj2 X) by A6, Th4;
A11: ex_sup_of proj2 X,L2 by A7, YELLOW_3:41;
then A12: ex_sup_of proj2 ([:f,g:] .: X),T2 by A5, A10, WAYBEL_0:def_31;
A13: proj1 ([:f,g:] .: X) = f .: (proj1 X) by A6, A9, Th4;
then ex_sup_of proj1 ([:f,g:] .: X),T1 by A4, A8, WAYBEL_0:def_31;
hence ex_sup_of [:f,g:] .: X,[:T1,T2:] by A12, YELLOW_3:41; ::_thesis: "\/" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("\/" (X,[:L1,L2:]))
hence sup ([:f,g:] .: X) = [(sup (f .: (proj1 X))),(sup (g .: (proj2 X)))] by A13, A10, Th8
.= [(f . (sup (proj1 X))),(sup (g .: (proj2 X)))] by A4, A8, WAYBEL_0:def_31
.= [(f . (sup (proj1 X))),(g . (sup (proj2 X)))] by A5, A11, WAYBEL_0:def_31
.= [:f,g:] . ((sup (proj1 X)),(sup (proj2 X))) by A6, FUNCT_3:def_8
.= [:f,g:] . (sup X) by A7, Th8 ;
::_thesis: verum
end;
theorem Th13: :: WAYBEL20:13
for L being non empty antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_inf_of X,[:L,L:] holds
inf X in id the carrier of L
proof
let L be non empty antisymmetric RelStr ; ::_thesis: for X being Subset of [:L,L:] st X c= id the carrier of L & ex_inf_of X,[:L,L:] holds
inf X in id the carrier of L
let X be Subset of [:L,L:]; ::_thesis: ( X c= id the carrier of L & ex_inf_of X,[:L,L:] implies inf X in id the carrier of L )
assume ( X c= id the carrier of L & ex_inf_of X,[:L,L:] ) ; ::_thesis: inf X in id the carrier of L
then ( inf X = [(inf (proj1 X)),(inf (proj2 X))] & inf (proj1 X) = inf (proj2 X) ) by Th1, Th7;
hence inf X in id the carrier of L by RELAT_1:def_10; ::_thesis: verum
end;
theorem Th14: :: WAYBEL20:14
for L being non empty antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds
sup X in id the carrier of L
proof
let L be non empty antisymmetric RelStr ; ::_thesis: for X being Subset of [:L,L:] st X c= id the carrier of L & ex_sup_of X,[:L,L:] holds
sup X in id the carrier of L
let X be Subset of [:L,L:]; ::_thesis: ( X c= id the carrier of L & ex_sup_of X,[:L,L:] implies sup X in id the carrier of L )
assume ( X c= id the carrier of L & ex_sup_of X,[:L,L:] ) ; ::_thesis: sup X in id the carrier of L
then ( sup X = [(sup (proj1 X)),(sup (proj2 X))] & sup (proj1 X) = sup (proj2 X) ) by Th1, Th8;
hence sup X in id the carrier of L by RELAT_1:def_10; ::_thesis: verum
end;
theorem Th15: :: WAYBEL20:15
for L, M being non empty RelStr st L,M are_isomorphic & L is reflexive holds
M is reflexive
proof
let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is reflexive implies M is reflexive )
assume that
A1: L,M are_isomorphic and
A2: L is reflexive ; ::_thesis: M is reflexive
let x be Element of M; :: according to YELLOW_0:def_1 ::_thesis: x <= x
M,L are_isomorphic by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3: f is isomorphic by WAYBEL_1:def_8;
reconsider fx = f . x as Element of L ;
fx <= fx by A2, YELLOW_0:def_1;
hence x <= x by A3, WAYBEL_0:66; ::_thesis: verum
end;
theorem Th16: :: WAYBEL20:16
for L, M being non empty RelStr st L,M are_isomorphic & L is transitive holds
M is transitive
proof
let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is transitive implies M is transitive )
assume that
A1: L,M are_isomorphic and
A2: L is transitive ; ::_thesis: M is transitive
M,L are_isomorphic by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3: f is isomorphic by WAYBEL_1:def_8;
let x, y, z be Element of M; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume A4: ( x <= y & y <= z ) ; ::_thesis: x <= z
reconsider fz = f . z as Element of L ;
reconsider fy = f . y as Element of L ;
reconsider fx = f . x as Element of L ;
( fx <= fy & fy <= fz ) by A3, A4, WAYBEL_0:66;
then fx <= fz by A2, YELLOW_0:def_2;
hence x <= z by A3, WAYBEL_0:66; ::_thesis: verum
end;
theorem Th17: :: WAYBEL20:17
for L, M being non empty RelStr st L,M are_isomorphic & L is antisymmetric holds
M is antisymmetric
proof
let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is antisymmetric implies M is antisymmetric )
assume that
A1: L,M are_isomorphic and
A2: L is antisymmetric ; ::_thesis: M is antisymmetric
M,L are_isomorphic by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3: f is isomorphic by WAYBEL_1:def_8;
let x, y be Element of M; :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
assume A4: ( x <= y & y <= x ) ; ::_thesis: x = y
reconsider fy = f . y as Element of L ;
reconsider fx = f . x as Element of L ;
( fx <= fy & fy <= fx ) by A3, A4, WAYBEL_0:66;
then ( dom f = the carrier of M & fx = fy ) by A2, FUNCT_2:def_1, YELLOW_0:def_3;
hence x = y by A3, FUNCT_1:def_4; ::_thesis: verum
end;
theorem Th18: :: WAYBEL20:18
for L, M being non empty RelStr st L,M are_isomorphic & L is complete holds
M is complete
proof
let L, M be non empty RelStr ; ::_thesis: ( L,M are_isomorphic & L is complete implies M is complete )
assume that
A1: L,M are_isomorphic and
A2: L is complete ; ::_thesis: M is complete
let X be Subset of M; :: according to LATTICE5:def_2 ::_thesis: ex b1 being Element of the carrier of M st
( b1 is_<=_than X & ( for b2 being Element of the carrier of M holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
M,L are_isomorphic by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3: f is isomorphic by WAYBEL_1:def_8;
reconsider fX = f .: X as Subset of L ;
consider fa being Element of L such that
A4: fa is_<=_than fX and
A5: for fb being Element of L st fb is_<=_than fX holds
fb <= fa by A2, LATTICE5:def_2;
set a = (f ") . fa;
A6: rng f = the carrier of L by A3, WAYBEL_0:66;
then (f ") . fa in dom f by A3, FUNCT_1:32;
then reconsider a = (f ") . fa as Element of M ;
A7: fa = f . a by A3, A6, FUNCT_1:35;
take a ; ::_thesis: ( a is_<=_than X & ( for b1 being Element of the carrier of M holds
( not b1 is_<=_than X or b1 <= a ) ) )
A8: dom f = the carrier of M by FUNCT_2:def_1;
hereby :: according to LATTICE3:def_8 ::_thesis: for b1 being Element of the carrier of M holds
( not b1 is_<=_than X or b1 <= a )
let b be Element of M; ::_thesis: ( b in X implies a <= b )
assume A9: b in X ; ::_thesis: a <= b
reconsider fb = f . b as Element of L ;
fb in fX by A8, A9, FUNCT_1:def_6;
then fa <= fb by A4, LATTICE3:def_8;
hence a <= b by A3, A7, WAYBEL_0:66; ::_thesis: verum
end;
let b be Element of M; ::_thesis: ( not b is_<=_than X or b <= a )
assume A10: b is_<=_than X ; ::_thesis: b <= a
reconsider fb = f . b as Element of L ;
fb is_<=_than fX
proof
let fc be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not fc in fX or fb <= fc )
assume fc in fX ; ::_thesis: fb <= fc
then consider c being set such that
A11: c in dom f and
A12: c in X and
A13: fc = f . c by FUNCT_1:def_6;
reconsider c = c as Element of M by A11;
b <= c by A10, A12, LATTICE3:def_8;
hence fb <= fc by A3, A13, WAYBEL_0:66; ::_thesis: verum
end;
then fb <= fa by A5;
hence b <= a by A3, A7, WAYBEL_0:66; ::_thesis: verum
end;
theorem Th19: :: WAYBEL20:19
for L being non empty transitive RelStr
for k being Function of L,L st k is infs-preserving holds
corestr k is infs-preserving
proof
let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is infs-preserving holds
corestr k is infs-preserving
let k be Function of L,L; ::_thesis: ( k is infs-preserving implies corestr k is infs-preserving )
assume A1: k is infs-preserving ; ::_thesis: corestr k is infs-preserving
let X be Subset of L; :: according to WAYBEL_0:def_32 ::_thesis: corestr k preserves_inf_of X
assume A2: ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (corestr k) .: X, Image k & "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) )
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
A4: k preserves_inf_of X by A1, WAYBEL_0:def_32;
then A5: ex_inf_of k .: X,L by A2, WAYBEL_0:def_30;
reconsider fX = (corestr k) .: X as Subset of (Image k) ;
dom k = the carrier of L by FUNCT_2:def_1;
then ( rng k = the carrier of (Image k) & k . (inf X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15;
then "/\" (fX,L) is Element of (Image k) by A4, A3, A2, WAYBEL_0:def_30;
hence ex_inf_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:63; ::_thesis: "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L))
inf (k .: X) = k . (inf X) by A4, A2, WAYBEL_0:def_30;
hence "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) by A3, A5, YELLOW_0:63; ::_thesis: verum
end;
theorem :: WAYBEL20:20
for L being non empty transitive RelStr
for k being Function of L,L st k is filtered-infs-preserving holds
corestr k is filtered-infs-preserving
proof
let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is filtered-infs-preserving holds
corestr k is filtered-infs-preserving
let k be Function of L,L; ::_thesis: ( k is filtered-infs-preserving implies corestr k is filtered-infs-preserving )
assume A1: k is filtered-infs-preserving ; ::_thesis: corestr k is filtered-infs-preserving
let X be Subset of L; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or corestr k preserves_inf_of X )
assume ( not X is empty & X is filtered ) ; ::_thesis: corestr k preserves_inf_of X
then A2: k preserves_inf_of X by A1, WAYBEL_0:def_36;
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
assume A4: ex_inf_of X,L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (corestr k) .: X, Image k & "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) )
then A5: ex_inf_of k .: X,L by A2, WAYBEL_0:def_30;
reconsider fX = (corestr k) .: X as Subset of (Image k) ;
dom k = the carrier of L by FUNCT_2:def_1;
then ( rng k = the carrier of (Image k) & k . (inf X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15;
then "/\" (fX,L) is Element of (Image k) by A2, A3, A4, WAYBEL_0:def_30;
hence ex_inf_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:63; ::_thesis: "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L))
inf (k .: X) = k . (inf X) by A2, A4, WAYBEL_0:def_30;
hence "/\" (((corestr k) .: X),(Image k)) = (corestr k) . ("/\" (X,L)) by A3, A5, YELLOW_0:63; ::_thesis: verum
end;
theorem :: WAYBEL20:21
for L being non empty transitive RelStr
for k being Function of L,L st k is sups-preserving holds
corestr k is sups-preserving
proof
let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is sups-preserving holds
corestr k is sups-preserving
let k be Function of L,L; ::_thesis: ( k is sups-preserving implies corestr k is sups-preserving )
assume A1: k is sups-preserving ; ::_thesis: corestr k is sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def_33 ::_thesis: corestr k preserves_sup_of X
assume A2: ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (corestr k) .: X, Image k & "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) )
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
A4: k preserves_sup_of X by A1, WAYBEL_0:def_33;
then A5: ex_sup_of k .: X,L by A2, WAYBEL_0:def_31;
reconsider fX = (corestr k) .: X as Subset of (Image k) ;
dom k = the carrier of L by FUNCT_2:def_1;
then ( rng k = the carrier of (Image k) & k . (sup X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15;
then "\/" (fX,L) is Element of (Image k) by A4, A3, A2, WAYBEL_0:def_31;
hence ex_sup_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:64; ::_thesis: "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L))
sup (k .: X) = k . (sup X) by A4, A2, WAYBEL_0:def_31;
hence "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) by A3, A5, YELLOW_0:64; ::_thesis: verum
end;
theorem Th22: :: WAYBEL20:22
for L being non empty transitive RelStr
for k being Function of L,L st k is directed-sups-preserving holds
corestr k is directed-sups-preserving
proof
let L be non empty transitive RelStr ; ::_thesis: for k being Function of L,L st k is directed-sups-preserving holds
corestr k is directed-sups-preserving
let k be Function of L,L; ::_thesis: ( k is directed-sups-preserving implies corestr k is directed-sups-preserving )
assume A1: k is directed-sups-preserving ; ::_thesis: corestr k is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or corestr k preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: corestr k preserves_sup_of X
then A2: k preserves_sup_of X by A1, WAYBEL_0:def_37;
set f = corestr k;
A3: k = corestr k by WAYBEL_1:30;
assume A4: ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (corestr k) .: X, Image k & "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) )
then A5: ex_sup_of k .: X,L by A2, WAYBEL_0:def_31;
reconsider fX = (corestr k) .: X as Subset of (Image k) ;
dom k = the carrier of L by FUNCT_2:def_1;
then ( rng k = the carrier of (Image k) & k . (sup X) in rng k ) by FUNCT_1:def_3, YELLOW_0:def_15;
then "\/" (fX,L) is Element of (Image k) by A2, A3, A4, WAYBEL_0:def_31;
hence ex_sup_of (corestr k) .: X, Image k by A3, A5, YELLOW_0:64; ::_thesis: "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L))
sup (k .: X) = k . (sup X) by A2, A4, WAYBEL_0:def_31;
hence "\/" (((corestr k) .: X),(Image k)) = (corestr k) . ("\/" (X,L)) by A3, A5, YELLOW_0:64; ::_thesis: verum
end;
theorem Th23: :: WAYBEL20:23
for S, T being non empty reflexive antisymmetric RelStr
for f being Function of S,T st f is filtered-infs-preserving holds
f is monotone
proof
let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of S,T st f is filtered-infs-preserving holds
f is monotone
let f be Function of S,T; ::_thesis: ( f is filtered-infs-preserving implies f is monotone )
assume A1: f is filtered-infs-preserving ; ::_thesis: f is monotone
let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y )
assume A2: x <= y ; ::_thesis: f . x <= f . y
A3: dom f = the carrier of S by FUNCT_2:def_1;
A4: for b being Element of S st {x,y} is_>=_than b holds
x >= b by YELLOW_0:8;
A5: x <= x ;
then A6: {x,y} is_>=_than x by A2, YELLOW_0:8;
then A7: ex_inf_of {x,y},S by A4, YELLOW_0:31;
for a, b being Element of S st a in {x,y} & b in {x,y} holds
ex z being Element of S st
( z in {x,y} & a >= z & b >= z )
proof
let a, b be Element of S; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of S st
( z in {x,y} & a >= z & b >= z ) )
assume A8: ( a in {x,y} & b in {x,y} ) ; ::_thesis: ex z being Element of S st
( z in {x,y} & a >= z & b >= z )
take x ; ::_thesis: ( x in {x,y} & a >= x & b >= x )
thus x in {x,y} by TARSKI:def_2; ::_thesis: ( a >= x & b >= x )
thus ( a >= x & b >= x ) by A2, A5, A8, TARSKI:def_2; ::_thesis: verum
end;
then ( {x,y} is filtered & not {x,y} is empty ) by WAYBEL_0:def_2;
then A9: f preserves_inf_of {x,y} by A1, WAYBEL_0:def_36;
x = inf {x,y} by A6, A4, YELLOW_0:31;
then inf (f .: {x,y}) = f . x by A7, A9, WAYBEL_0:def_30;
then A10: f . x = inf {(f . x),(f . y)} by A3, FUNCT_1:60;
f .: {x,y} = {(f . x),(f . y)} by A3, FUNCT_1:60;
then ex_inf_of {(f . x),(f . y)},T by A7, A9, WAYBEL_0:def_30;
then {(f . x),(f . y)} is_>=_than f . x by A10, YELLOW_0:def_10;
hence f . x <= f . y by YELLOW_0:8; ::_thesis: verum
end;
theorem Th24: :: WAYBEL20:24
for S, T being non empty RelStr
for f being Function of S,T st f is monotone holds
for X being Subset of S st X is filtered holds
f .: X is filtered
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is monotone holds
for X being Subset of S st X is filtered holds
f .: X is filtered
let f be Function of S,T; ::_thesis: ( f is monotone implies for X being Subset of S st X is filtered holds
f .: X is filtered )
assume A1: f is monotone ; ::_thesis: for X being Subset of S st X is filtered holds
f .: X is filtered
let X be Subset of S; ::_thesis: ( X is filtered implies f .: X is filtered )
assume A2: X is filtered ; ::_thesis: f .: X is filtered
let x, y be Element of T; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in f .: X or not y in f .: X or ex b1 being Element of the carrier of T st
( b1 in f .: X & b1 <= x & b1 <= y ) )
assume x in f .: X ; ::_thesis: ( not y in f .: X or ex b1 being Element of the carrier of T st
( b1 in f .: X & b1 <= x & b1 <= y ) )
then consider a being set such that
A3: a in the carrier of S and
A4: a in X and
A5: x = f . a by FUNCT_2:64;
assume y in f .: X ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in f .: X & b1 <= x & b1 <= y )
then consider b being set such that
A6: b in the carrier of S and
A7: b in X and
A8: y = f . b by FUNCT_2:64;
reconsider a = a, b = b as Element of S by A3, A6;
consider c being Element of S such that
A9: c in X and
A10: ( c <= a & c <= b ) by A2, A4, A7, WAYBEL_0:def_2;
take z = f . c; ::_thesis: ( z in f .: X & z <= x & z <= y )
thus z in f .: X by A9, FUNCT_2:35; ::_thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A1, A5, A8, A10, WAYBEL_1:def_2; ::_thesis: verum
end;
theorem Th25: :: WAYBEL20:25
for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds
g * f is infs-preserving
proof
let L1, L2, L3 be non empty RelStr ; ::_thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds
g * f is infs-preserving
let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is infs-preserving & g is infs-preserving holds
g * f is infs-preserving
let g be Function of L2,L3; ::_thesis: ( f is infs-preserving & g is infs-preserving implies g * f is infs-preserving )
assume that
A1: f is infs-preserving and
A2: g is infs-preserving ; ::_thesis: g * f is infs-preserving
set gf = g * f;
let X be Subset of L1; :: according to WAYBEL_0:def_32 ::_thesis: g * f preserves_inf_of X
assume A3: ex_inf_of X,L1 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (g * f) .: X,L3 & "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1)) )
set fX = f .: X;
set gfX = (g * f) .: X;
A4: f preserves_inf_of X by A1, WAYBEL_0:def_32;
then A5: ( (g * f) .: X = g .: (f .: X) & ex_inf_of f .: X,L2 ) by A3, RELAT_1:126, WAYBEL_0:def_30;
A6: dom f = the carrier of L1 by FUNCT_2:def_1;
A7: g preserves_inf_of f .: X by A2, WAYBEL_0:def_32;
hence ex_inf_of (g * f) .: X,L3 by A5, WAYBEL_0:def_30; ::_thesis: "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1))
thus inf ((g * f) .: X) = g . (inf (f .: X)) by A7, A5, WAYBEL_0:def_30
.= g . (f . (inf X)) by A3, A4, WAYBEL_0:def_30
.= (g * f) . (inf X) by A6, FUNCT_1:13 ; ::_thesis: verum
end;
theorem :: WAYBEL20:26
for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving
proof
let L1, L2, L3 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving
let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving
let g be Function of L2,L3; ::_thesis: ( f is filtered-infs-preserving & g is filtered-infs-preserving implies g * f is filtered-infs-preserving )
assume that
A1: f is filtered-infs-preserving and
A2: g is filtered-infs-preserving ; ::_thesis: g * f is filtered-infs-preserving
set gf = g * f;
let X be Subset of L1; :: according to WAYBEL_0:def_36 ::_thesis: ( X is empty or not X is filtered or g * f preserves_inf_of X )
assume that
A3: ( not X is empty & X is filtered ) and
A4: ex_inf_of X,L1 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (g * f) .: X,L3 & "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1)) )
set xx = the Element of X;
set fX = f .: X;
set gfX = (g * f) .: X;
A5: f preserves_inf_of X by A1, A3, WAYBEL_0:def_36;
then A6: ( (g * f) .: X = g .: (f .: X) & ex_inf_of f .: X,L2 ) by A4, RELAT_1:126, WAYBEL_0:def_30;
the Element of X in X by A3;
then f . the Element of X in f .: X by FUNCT_2:35;
then ( not f .: X is empty & f .: X is filtered ) by A1, A3, Th23, Th24;
then A7: g preserves_inf_of f .: X by A2, WAYBEL_0:def_36;
hence ex_inf_of (g * f) .: X,L3 by A6, WAYBEL_0:def_30; ::_thesis: "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1))
A8: dom f = the carrier of L1 by FUNCT_2:def_1;
thus inf ((g * f) .: X) = g . (inf (f .: X)) by A7, A6, WAYBEL_0:def_30
.= g . (f . (inf X)) by A4, A5, WAYBEL_0:def_30
.= (g * f) . (inf X) by A8, FUNCT_1:13 ; ::_thesis: verum
end;
theorem :: WAYBEL20:27
for L1, L2, L3 being non empty RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving
proof
let L1, L2, L3 be non empty RelStr ; ::_thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving
let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving
let g be Function of L2,L3; ::_thesis: ( f is sups-preserving & g is sups-preserving implies g * f is sups-preserving )
assume that
A1: f is sups-preserving and
A2: g is sups-preserving ; ::_thesis: g * f is sups-preserving
set gf = g * f;
let X be Subset of L1; :: according to WAYBEL_0:def_33 ::_thesis: g * f preserves_sup_of X
assume A3: ex_sup_of X,L1 ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (g * f) .: X,L3 & "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1)) )
set fX = f .: X;
set gfX = (g * f) .: X;
A4: f preserves_sup_of X by A1, WAYBEL_0:def_33;
then A5: ( (g * f) .: X = g .: (f .: X) & ex_sup_of f .: X,L2 ) by A3, RELAT_1:126, WAYBEL_0:def_31;
A6: dom f = the carrier of L1 by FUNCT_2:def_1;
A7: g preserves_sup_of f .: X by A2, WAYBEL_0:def_33;
hence ex_sup_of (g * f) .: X,L3 by A5, WAYBEL_0:def_31; ::_thesis: "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1))
thus sup ((g * f) .: X) = g . (sup (f .: X)) by A7, A5, WAYBEL_0:def_31
.= g . (f . (sup X)) by A3, A4, WAYBEL_0:def_31
.= (g * f) . (sup X) by A6, FUNCT_1:13 ; ::_thesis: verum
end;
theorem :: WAYBEL20:28
for L1, L2, L3 being non empty reflexive antisymmetric RelStr
for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
proof
let L1, L2, L3 be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
let f be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
let g be Function of L2,L3; ::_thesis: ( f is directed-sups-preserving & g is directed-sups-preserving implies g * f is directed-sups-preserving )
assume that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving ; ::_thesis: g * f is directed-sups-preserving
set gf = g * f;
let X be Subset of L1; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or g * f preserves_sup_of X )
assume that
A3: ( not X is empty & X is directed ) and
A4: ex_sup_of X,L1 ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (g * f) .: X,L3 & "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1)) )
set xx = the Element of X;
set fX = f .: X;
set gfX = (g * f) .: X;
A5: f preserves_sup_of X by A1, A3, WAYBEL_0:def_37;
then A6: ( (g * f) .: X = g .: (f .: X) & ex_sup_of f .: X,L2 ) by A4, RELAT_1:126, WAYBEL_0:def_31;
the Element of X in X by A3;
then f . the Element of X in f .: X by FUNCT_2:35;
then ( not f .: X is empty & f .: X is directed ) by A1, A3, WAYBEL17:3, YELLOW_2:15;
then A7: g preserves_sup_of f .: X by A2, WAYBEL_0:def_37;
hence ex_sup_of (g * f) .: X,L3 by A6, WAYBEL_0:def_31; ::_thesis: "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1))
A8: dom f = the carrier of L1 by FUNCT_2:def_1;
thus sup ((g * f) .: X) = g . (sup (f .: X)) by A7, A6, WAYBEL_0:def_31
.= g . (f . (sup X)) by A4, A5, WAYBEL_0:def_31
.= (g * f) . (sup X) by A8, FUNCT_1:13 ; ::_thesis: verum
end;
begin
theorem :: WAYBEL20:29
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
product J is lower-bounded
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
product J is lower-bounded
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) implies product J is lower-bounded )
assume A1: for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ; ::_thesis: product J is lower-bounded
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
f . i = Bottom (J . i) by A2;
hence f . i is Element of (J . i) ; ::_thesis: verum
end;
dom f = I by PARTFUN1:def_2;
then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27;
take f ; :: according to YELLOW_0:def_4 ::_thesis: f is_<=_than the carrier of (product J)
let b be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not b in the carrier of (product J) or f <= b )
assume b in the carrier of (product J) ; ::_thesis: f <= b
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_b_._i
let i be Element of I; ::_thesis: f . i <= b . i
( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2;
hence f . i <= b . i by YELLOW_0:44; ::_thesis: verum
end;
hence f <= b by WAYBEL_3:28; ::_thesis: verum
end;
theorem :: WAYBEL20:30
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
product J is upper-bounded
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
product J is upper-bounded
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) implies product J is upper-bounded )
assume A1: for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ; ::_thesis: product J is upper-bounded
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Top (J . $1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
f . i = Top (J . i) by A2;
hence f . i is Element of (J . i) ; ::_thesis: verum
end;
dom f = I by PARTFUN1:def_2;
then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27;
take f ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of (product J) is_<=_than f
let b be Element of (product J); :: according to LATTICE3:def_9 ::_thesis: ( not b in the carrier of (product J) or b <= f )
assume b in the carrier of (product J) ; ::_thesis: b <= f
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_b_._i
let i be Element of I; ::_thesis: f . i >= b . i
( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2;
hence f . i >= b . i by YELLOW_0:45; ::_thesis: verum
end;
hence b <= f by WAYBEL_3:28; ::_thesis: verum
end;
theorem :: WAYBEL20:31
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) implies for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i) )
assume A1: for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ; ::_thesis: for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
f . i = Bottom (J . i) by A2;
hence f . i is Element of (J . i) ; ::_thesis: verum
end;
dom f = I by PARTFUN1:def_2;
then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27;
let i be Element of I; ::_thesis: (Bottom (product J)) . i = Bottom (J . i)
A4: {} is_<=_than f by YELLOW_0:6;
A5: now__::_thesis:_for_c_being_Element_of_(product_J)_st_{}_is_<=_than_c_&_(_for_b_being_Element_of_(product_J)_st_{}_is_<=_than_b_holds_
b_>=_c_)_holds_
c_=_f
let c be Element of (product J); ::_thesis: ( {} is_<=_than c & ( for b being Element of (product J) st {} is_<=_than b holds
b >= c ) implies c = f )
assume that
{} is_<=_than c and
A6: for b being Element of (product J) st {} is_<=_than b holds
b >= c ; ::_thesis: c = f
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_c_._i
let i be Element of I; ::_thesis: f . i <= c . i
( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2;
hence f . i <= c . i by YELLOW_0:44; ::_thesis: verum
end;
then A7: f <= c by WAYBEL_3:28;
for i being Element of I holds J . i is antisymmetric by A1;
then A8: product J is antisymmetric by WAYBEL_3:30;
c <= f by A6, YELLOW_0:6;
hence c = f by A8, A7, YELLOW_0:def_3; ::_thesis: verum
end;
A9: now__::_thesis:_for_a_being_Element_of_(product_J)_st_{}_is_<=_than_a_holds_
f_<=_a
let a be Element of (product J); ::_thesis: ( {} is_<=_than a implies f <= a )
assume {} is_<=_than a ; ::_thesis: f <= a
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_a_._i
let i be Element of I; ::_thesis: f . i <= a . i
( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2;
hence f . i <= a . i by YELLOW_0:44; ::_thesis: verum
end;
hence f <= a by WAYBEL_3:28; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(product_J)_st_{}_is_<=_than_b_holds_
f_<=_b
let b be Element of (product J); ::_thesis: ( {} is_<=_than b implies f <= b )
assume {} is_<=_than b ; ::_thesis: f <= b
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_<=_b_._i
let i be Element of I; ::_thesis: f . i <= b . i
( f . i = Bottom (J . i) & J . i is non empty antisymmetric lower-bounded RelStr ) by A1, A2;
hence f . i <= b . i by YELLOW_0:44; ::_thesis: verum
end;
hence f <= b by WAYBEL_3:28; ::_thesis: verum
end;
then ex_sup_of {} , product J by A4, A5, YELLOW_0:def_7;
then f = "\/" ({},(product J)) by A4, A9, YELLOW_0:def_9;
hence (Bottom (product J)) . i = Bottom (J . i) by A2; ::_thesis: verum
end;
theorem :: WAYBEL20:32
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ) implies for i being Element of I holds (Top (product J)) . i = Top (J . i) )
assume A1: for i being Element of I holds J . i is antisymmetric upper-bounded RelStr ; ::_thesis: for i being Element of I holds (Top (product J)) . i = Top (J . i)
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Top (J . $1);
consider f being ManySortedSet of I such that
A2: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A3: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
f . i = Top (J . i) by A2;
hence f . i is Element of (J . i) ; ::_thesis: verum
end;
dom f = I by PARTFUN1:def_2;
then reconsider f = f as Element of (product J) by A3, WAYBEL_3:27;
let i be Element of I; ::_thesis: (Top (product J)) . i = Top (J . i)
A4: {} is_>=_than f by YELLOW_0:6;
A5: now__::_thesis:_for_c_being_Element_of_(product_J)_st_{}_is_>=_than_c_&_(_for_b_being_Element_of_(product_J)_st_{}_is_>=_than_b_holds_
b_<=_c_)_holds_
c_=_f
let c be Element of (product J); ::_thesis: ( {} is_>=_than c & ( for b being Element of (product J) st {} is_>=_than b holds
b <= c ) implies c = f )
assume that
{} is_>=_than c and
A6: for b being Element of (product J) st {} is_>=_than b holds
b <= c ; ::_thesis: c = f
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_c_._i
let i be Element of I; ::_thesis: f . i >= c . i
( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2;
hence f . i >= c . i by YELLOW_0:45; ::_thesis: verum
end;
then A7: f >= c by WAYBEL_3:28;
for i being Element of I holds J . i is antisymmetric by A1;
then A8: product J is antisymmetric by WAYBEL_3:30;
c >= f by A6, YELLOW_0:6;
hence c = f by A8, A7, YELLOW_0:def_3; ::_thesis: verum
end;
A9: now__::_thesis:_for_a_being_Element_of_(product_J)_st_{}_is_>=_than_a_holds_
f_>=_a
let a be Element of (product J); ::_thesis: ( {} is_>=_than a implies f >= a )
assume {} is_>=_than a ; ::_thesis: f >= a
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_a_._i
let i be Element of I; ::_thesis: f . i >= a . i
( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2;
hence f . i >= a . i by YELLOW_0:45; ::_thesis: verum
end;
hence f >= a by WAYBEL_3:28; ::_thesis: verum
end;
now__::_thesis:_for_b_being_Element_of_(product_J)_st_{}_is_>=_than_b_holds_
f_>=_b
let b be Element of (product J); ::_thesis: ( {} is_>=_than b implies f >= b )
assume {} is_>=_than b ; ::_thesis: f >= b
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_>=_b_._i
let i be Element of I; ::_thesis: f . i >= b . i
( f . i = Top (J . i) & J . i is non empty antisymmetric upper-bounded RelStr ) by A1, A2;
hence f . i >= b . i by YELLOW_0:45; ::_thesis: verum
end;
hence f >= b by WAYBEL_3:28; ::_thesis: verum
end;
then ex_inf_of {} , product J by A4, A5, YELLOW_0:def_8;
then f = "/\" ({},(product J)) by A4, A9, YELLOW_0:def_10;
hence (Top (product J)) . i = Top (J . i) by A2; ::_thesis: verum
end;
theorem :: WAYBEL20:33
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds
product J is continuous
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds
product J is continuous
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete continuous LATTICE ) implies product J is continuous )
assume A1: for i being Element of I holds J . i is complete continuous LATTICE ; ::_thesis: product J is continuous
A2: for i being Element of I holds J . i is complete LATTICE by A1;
set pJ = product J;
reconsider pJ9 = product J as complete LATTICE by A2, WAYBEL_3:31;
hereby :: according to WAYBEL_3:def_6 ::_thesis: ( product J is up-complete & product J is satisfying_axiom_of_approximation )
let x be Element of (product J); ::_thesis: ( not waybelow x is empty & waybelow x is directed )
reconsider x9 = x as Element of pJ9 ;
not waybelow x9 is empty ;
hence not waybelow x is empty ; ::_thesis: waybelow x is directed
waybelow x9 is directed ;
hence waybelow x is directed ; ::_thesis: verum
end;
pJ9 is up-complete ;
hence product J is up-complete ; ::_thesis: product J is satisfying_axiom_of_approximation
let x be Element of (product J); :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),(product J))
set swx = sup (waybelow x);
now__::_thesis:_(_dom_x_=_I_&_dom_(sup_(waybelow_x))_=_I_&_(_for_i_being_set_st_i_in_I_holds_
x_._i_=_(sup_(waybelow_x))_._i_)_)
thus dom x = I by WAYBEL_3:27; ::_thesis: ( dom (sup (waybelow x)) = I & ( for i being set st i in I holds
x . i = (sup (waybelow x)) . i ) )
thus dom (sup (waybelow x)) = I by WAYBEL_3:27; ::_thesis: for i being set st i in I holds
x . i = (sup (waybelow x)) . i
let i be set ; ::_thesis: ( i in I implies x . i = (sup (waybelow x)) . i )
assume i in I ; ::_thesis: x . i = (sup (waybelow x)) . i
then reconsider i9 = i as Element of I ;
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_pi_((waybelow_x),i9)_implies_a_in_waybelow_(x_._i9)_)_&_(_a_in_waybelow_(x_._i9)_implies_a_in_pi_((waybelow_x),i9)_)_)
reconsider K = {i9} as finite Subset of I ;
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
let a be set ; ::_thesis: ( ( a in pi ((waybelow x),i9) implies a in waybelow (x . i9) ) & ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) ) )
consider g being ManySortedSet of I such that
A3: for i being Element of I holds g . i = H1(i) from PBOOLE:sch_5();
set f = g +* (i,a);
hereby ::_thesis: ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) )
assume a in pi ((waybelow x),i9) ; ::_thesis: a in waybelow (x . i9)
then consider f being Function such that
A4: f in waybelow x and
A5: a = f . i by CARD_3:def_6;
reconsider f = f as Element of (product J) by A4;
f << x by A4, WAYBEL_3:7;
then f . i9 << x . i9 by A2, WAYBEL_3:33;
hence a in waybelow (x . i9) by A5; ::_thesis: verum
end;
A6: dom g = I by PARTFUN1:def_2;
then A7: dom (g +* (i,a)) = I by FUNCT_7:30;
assume A8: a in waybelow (x . i9) ; ::_thesis: a in pi ((waybelow x),i9)
now__::_thesis:_for_j_being_Element_of_I_holds_(g_+*_(i,a))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: (g +* (i,a)) . b1 is Element of (J . b1)
percases ( i9 = j or i9 <> j ) ;
suppose i9 = j ; ::_thesis: (g +* (i,a)) . b1 is Element of (J . b1)
hence (g +* (i,a)) . j is Element of (J . j) by A8, A6, FUNCT_7:31; ::_thesis: verum
end;
suppose i9 <> j ; ::_thesis: (g +* (i,a)) . b1 is Element of (J . b1)
then (g +* (i,a)) . j = g . j by FUNCT_7:32
.= Bottom (J . j) by A3 ;
hence (g +* (i,a)) . j is Element of (J . j) ; ::_thesis: verum
end;
end;
end;
then reconsider f = g +* (i,a) as Element of (product J) by A7, WAYBEL_3:27;
A9: now__::_thesis:_for_j_being_Element_of_I_holds_f_._j_<<_x_._j
let j be Element of I; ::_thesis: f . b1 << x . b1
percases ( i9 = j or i9 <> j ) ;
supposeA10: i9 = j ; ::_thesis: f . b1 << x . b1
f . i9 = a by A6, FUNCT_7:31;
hence f . j << x . j by A8, A10, WAYBEL_3:7; ::_thesis: verum
end;
supposeA11: i9 <> j ; ::_thesis: f . b1 << x . b1
A12: J . j is complete LATTICE by A1;
f . j = g . j by A11, FUNCT_7:32
.= Bottom (J . j) by A3 ;
hence f . j << x . j by A12, WAYBEL_3:4; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_j_being_Element_of_I_st_not_j_in_K_holds_
f_._j_=_Bottom_(J_._j)
let j be Element of I; ::_thesis: ( not j in K implies f . j = Bottom (J . j) )
assume not j in K ; ::_thesis: f . j = Bottom (J . j)
then j <> i9 by TARSKI:def_1;
hence f . j = g . j by FUNCT_7:32
.= Bottom (J . j) by A3 ;
::_thesis: verum
end;
then f << x by A2, A9, WAYBEL_3:33;
then A13: f in waybelow x ;
a = f . i9 by A6, FUNCT_7:31;
hence a in pi ((waybelow x),i9) by A13, CARD_3:def_6; ::_thesis: verum
end;
then A14: pi ((waybelow x),i9) = waybelow (x . i9) by TARSKI:1;
( (sup (waybelow x)) . i9 = sup (pi ((waybelow x),i9)) & J . i9 is satisfying_axiom_of_approximation ) by A1, A2, WAYBEL_3:32;
hence x . i = (sup (waybelow x)) . i by A14, WAYBEL_3:def_5; ::_thesis: verum
end;
hence x = "\/" ((waybelow x),(product J)) by FUNCT_1:2; ::_thesis: verum
end;
begin
theorem Th34: :: WAYBEL20:34
for L, T being complete continuous LATTICE
for g being CLHomomorphism of L,T
for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]
proof
let L, T be complete continuous LATTICE; ::_thesis: for g being CLHomomorphism of L,T
for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]
let g be CLHomomorphism of L,T; ::_thesis: for S being Subset of [:L,L:] st S = [:g,g:] " (id the carrier of T) holds
subrelstr S is CLSubFrame of [:L,L:]
let SL be Subset of [:L,L:]; ::_thesis: ( SL = [:g,g:] " (id the carrier of T) implies subrelstr SL is CLSubFrame of [:L,L:] )
assume A1: SL = [:g,g:] " (id the carrier of T) ; ::_thesis: subrelstr SL is CLSubFrame of [:L,L:]
set x = the Element of L;
A2: dom g = the carrier of L by FUNCT_2:def_1;
then A3: [ the Element of L, the Element of L] in [:(dom g),(dom g):] by ZFMISC_1:87;
[(g . the Element of L),(g . the Element of L)] in id the carrier of T by RELAT_1:def_10;
then ( dom [:g,g:] = [:(dom g),(dom g):] & [:g,g:] . ( the Element of L, the Element of L) in id the carrier of T ) by A2, FUNCT_3:def_8;
then reconsider nSL = SL as non empty Subset of [:L,L:] by A1, A3, FUNCT_1:def_7;
set pL = [:L,L:];
set pg = [:g,g:];
A4: ( g is infs-preserving & g is directed-sups-preserving ) by WAYBEL16:def_1;
A5: the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2;
A6: not subrelstr nSL is empty ;
A7: subrelstr SL is directed-sups-inheriting
proof
let X be directed Subset of (subrelstr SL); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,[:L,L:] or "\/" (X,[:L,L:]) in the carrier of (subrelstr SL) )
assume that
A8: X <> {} and
A9: ex_sup_of X,[:L,L:] ; ::_thesis: "\/" (X,[:L,L:]) in the carrier of (subrelstr SL)
reconsider X9 = X as non empty directed Subset of [:L,L:] by A6, A8, YELLOW_2:7;
[:g,g:] is directed-sups-preserving by A4, Th12;
then [:g,g:] preserves_sup_of X9 by WAYBEL_0:def_37;
then A10: sup ([:g,g:] .: X9) = [:g,g:] . (sup X9) by A9, WAYBEL_0:def_31;
X c= the carrier of (subrelstr SL) ;
then X c= SL by YELLOW_0:def_15;
then A11: [:g,g:] .: X c= [:g,g:] .: SL by RELAT_1:123;
( [:g,g:] .: SL c= id the carrier of T & ex_sup_of [:g,g:] .: X9,[:T,T:] ) by A1, FUNCT_1:75, YELLOW_0:17;
then A12: sup ([:g,g:] .: X9) in id the carrier of T by A11, Th14, XBOOLE_1:1;
consider x, y being set such that
A13: ( x in the carrier of L & y in the carrier of L ) and
A14: sup X9 = [x,y] by A5, ZFMISC_1:def_2;
[x,y] in [:(dom g),(dom g):] by A2, A13, ZFMISC_1:87;
then [x,y] in dom [:g,g:] by FUNCT_3:def_8;
then [x,y] in [:g,g:] " (id the carrier of T) by A14, A10, A12, FUNCT_1:def_7;
hence "\/" (X,[:L,L:]) in the carrier of (subrelstr SL) by A1, A14, YELLOW_0:def_15; ::_thesis: verum
end;
subrelstr SL is infs-inheriting
proof
let X be Subset of (subrelstr SL); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,[:L,L:] or "/\" (X,[:L,L:]) in the carrier of (subrelstr SL) )
assume A15: ex_inf_of X,[:L,L:] ; ::_thesis: "/\" (X,[:L,L:]) in the carrier of (subrelstr SL)
X c= the carrier of (subrelstr SL) ;
then A16: X c= SL by YELLOW_0:def_15;
then reconsider X9 = X as Subset of [:L,L:] by XBOOLE_1:1;
A17: ( [:g,g:] .: SL c= id the carrier of T & ex_inf_of [:g,g:] .: X9,[:T,T:] ) by A1, FUNCT_1:75, YELLOW_0:17;
[:g,g:] is infs-preserving by A4, Th9;
then [:g,g:] preserves_inf_of X9 by WAYBEL_0:def_32;
then A18: inf ([:g,g:] .: X9) = [:g,g:] . (inf X9) by A15, WAYBEL_0:def_30;
[:g,g:] .: X c= [:g,g:] .: SL by A16, RELAT_1:123;
then A19: inf ([:g,g:] .: X9) in id the carrier of T by A17, Th13, XBOOLE_1:1;
consider x, y being set such that
A20: ( x in the carrier of L & y in the carrier of L ) and
A21: inf X9 = [x,y] by A5, ZFMISC_1:def_2;
[x,y] in [:(dom g),(dom g):] by A2, A20, ZFMISC_1:87;
then [x,y] in dom [:g,g:] by FUNCT_3:def_8;
then [x,y] in [:g,g:] " (id the carrier of T) by A21, A18, A19, FUNCT_1:def_7;
hence "/\" (X,[:L,L:]) in the carrier of (subrelstr SL) by A1, A21, YELLOW_0:def_15; ::_thesis: verum
end;
hence subrelstr SL is CLSubFrame of [:L,L:] by A7; ::_thesis: verum
end;
definition
let L be RelStr ;
let R be Subset of [:L,L:];
assume A1: R is Equivalence_Relation of the carrier of L ;
func EqRel R -> Equivalence_Relation of the carrier of L equals :Def1: :: WAYBEL20:def 1
R;
correctness
coherence
R is Equivalence_Relation of the carrier of L;
by A1;
end;
:: deftheorem Def1 defines EqRel WAYBEL20:def_1_:_
for L being RelStr
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L holds
EqRel R = R;
definition
let L be non empty RelStr ;
let R be Subset of [:L,L:];
attrR is CLCongruence means :Def2: :: WAYBEL20:def 2
( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] );
end;
:: deftheorem Def2 defines CLCongruence WAYBEL20:def_2_:_
for L being non empty RelStr
for R being Subset of [:L,L:] holds
( R is CLCongruence iff ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ) );
theorem Th35: :: WAYBEL20:35
for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R
proof
let L be complete LATTICE; ::_thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R
let R be non empty Subset of [:L,L:]; ::_thesis: ( R is CLCongruence implies for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R )
assume A1: R is CLCongruence ; ::_thesis: for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R
let x be Element of L; ::_thesis: [(inf (Class ((EqRel R),x))),x] in R
set CRx = Class ((EqRel R),x);
reconsider SR = [:(Class ((EqRel R),x)),{x}:] as Subset of [:L,L:] ;
R is Equivalence_Relation of the carrier of L by A1, Def2;
then A2: R = EqRel R by Def1;
SR c= the carrier of (subrelstr R)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SR or a in the carrier of (subrelstr R) )
assume a in SR ; ::_thesis: a in the carrier of (subrelstr R)
then consider a1, a2 being set such that
A3: a1 in Class ((EqRel R),x) and
A4: a2 in {x} and
A5: a = [a1,a2] by ZFMISC_1:def_2;
a2 = x by A4, TARSKI:def_1;
then a in R by A2, A3, A5, EQREL_1:19;
hence a in the carrier of (subrelstr R) by YELLOW_0:def_15; ::_thesis: verum
end;
then reconsider SR9 = SR as Subset of (subrelstr R) ;
A6: ex_inf_of SR,[:L,L:] by YELLOW_0:17;
subrelstr R is CLSubFrame of [:L,L:] by A1, Def2;
then A7: "/\" (SR9,[:L,L:]) in the carrier of (subrelstr R) by A6, YELLOW_0:def_18;
A8: x in Class ((EqRel R),x) by EQREL_1:20;
inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7, YELLOW_0:17
.= [(inf (Class ((EqRel R),x))),(inf (proj2 SR))] by FUNCT_5:9
.= [(inf (Class ((EqRel R),x))),(inf {x})] by A8, FUNCT_5:9
.= [(inf (Class ((EqRel R),x))),x] by YELLOW_0:39 ;
hence [(inf (Class ((EqRel R),x))),x] in R by A7, YELLOW_0:def_15; ::_thesis: verum
end;
definition
let L be complete LATTICE;
let R be non empty Subset of [:L,L:];
assume B1: R is CLCongruence ;
func kernel_op R -> kernel Function of L,L means :Def3: :: WAYBEL20:def 3
for x being Element of L holds it . x = inf (Class ((EqRel R),x));
existence
ex b1 being kernel Function of L,L st
for x being Element of L holds b1 . x = inf (Class ((EqRel R),x))
proof
deffunc H1( Element of L) -> Element of the carrier of L = inf (Class ((EqRel R),$1));
consider k being Function of the carrier of L, the carrier of L such that
A1: for x being Element of L holds k . x = H1(x) from FUNCT_2:sch_4();
reconsider k = k as Function of L,L ;
R is Equivalence_Relation of the carrier of L by B1, Def2;
then A2: R = EqRel R by Def1;
A3: subrelstr R is CLSubFrame of [:L,L:] by B1, Def2;
A4: k is monotone
proof
let x, y be Element of L; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or k . x <= k . y )
assume A5: x <= y ; ::_thesis: k . x <= k . y
set CRy = Class ((EqRel R),y);
set CRx = Class ((EqRel R),x);
reconsider SR = {[(inf (Class ((EqRel R),x))),x],[(inf (Class ((EqRel R),y))),y]} as Subset of [:L,L:] ;
A6: inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7, YELLOW_0:17
.= [(inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))}),(inf (proj2 SR))] by FUNCT_5:13
.= [(inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))}),(inf {x,y})] by FUNCT_5:13 ;
( [(inf (Class ((EqRel R),x))),x] in R & [(inf (Class ((EqRel R),y))),y] in R ) by B1, Th35;
then SR c= R by ZFMISC_1:32;
then reconsider SR9 = SR as Subset of (subrelstr R) by YELLOW_0:def_15;
ex_inf_of SR,[:L,L:] by YELLOW_0:17;
then A7: "/\" (SR9,[:L,L:]) in the carrier of (subrelstr R) by A3, YELLOW_0:def_18;
inf {x,y} = x "/\" y by YELLOW_0:40
.= x by A5, YELLOW_0:25 ;
then [(inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))}),x] in R by A6, A7, YELLOW_0:def_15;
then inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} in Class ((EqRel R),x) by A2, EQREL_1:19;
then A8: inf (Class ((EqRel R),x)) <= inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} by YELLOW_2:22;
inf (Class ((EqRel R),y)) in {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} by TARSKI:def_2;
then A9: inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} <= inf (Class ((EqRel R),y)) by YELLOW_2:22;
( k . x = inf (Class ((EqRel R),x)) & k . y = inf (Class ((EqRel R),y)) ) by A1;
hence k . x <= k . y by A8, A9, YELLOW_0:def_2; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_L_holds_(k_*_k)_._x_=_k_._x
let x be Element of L; ::_thesis: (k * k) . x = k . x
set CRx = Class ((EqRel R),x);
[(inf (Class ((EqRel R),x))),x] in R by B1, Th35;
then inf (Class ((EqRel R),x)) in Class ((EqRel R),x) by A2, EQREL_1:19;
then A10: Class ((EqRel R),(inf (Class ((EqRel R),x)))) = Class ((EqRel R),x) by EQREL_1:23;
A11: k . x = inf (Class ((EqRel R),x)) by A1;
then k . (k . x) = inf (Class ((EqRel R),(inf (Class ((EqRel R),x))))) by A1;
hence (k * k) . x = k . x by A11, A10, FUNCT_2:15; ::_thesis: verum
end;
then k * k = k by FUNCT_2:63;
then k is idempotent by QUANTAL1:def_9;
then A12: k is projection by A4, WAYBEL_1:def_13;
now__::_thesis:_for_x_being_Element_of_L_holds_k_._x_<=_(id_L)_._x
let x be Element of L; ::_thesis: k . x <= (id L) . x
set CRx = Class ((EqRel R),x);
( x in Class ((EqRel R),x) & inf (Class ((EqRel R),x)) is_<=_than Class ((EqRel R),x) ) by EQREL_1:20, YELLOW_0:33;
then A13: inf (Class ((EqRel R),x)) <= x by LATTICE3:def_8;
k . x = inf (Class ((EqRel R),x)) by A1;
hence k . x <= (id L) . x by A13, FUNCT_1:18; ::_thesis: verum
end;
then k <= id L by YELLOW_2:9;
then reconsider k = k as kernel Function of L,L by A12, WAYBEL_1:def_15;
take k ; ::_thesis: for x being Element of L holds k . x = inf (Class ((EqRel R),x))
thus for x being Element of L holds k . x = inf (Class ((EqRel R),x)) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being kernel Function of L,L st ( for x being Element of L holds b1 . x = inf (Class ((EqRel R),x)) ) & ( for x being Element of L holds b2 . x = inf (Class ((EqRel R),x)) ) holds
b1 = b2
proof
let it1, it2 be kernel Function of L,L; ::_thesis: ( ( for x being Element of L holds it1 . x = inf (Class ((EqRel R),x)) ) & ( for x being Element of L holds it2 . x = inf (Class ((EqRel R),x)) ) implies it1 = it2 )
assume that
A14: for x being Element of L holds it1 . x = inf (Class ((EqRel R),x)) and
A15: for x being Element of L holds it2 . x = inf (Class ((EqRel R),x)) ; ::_thesis: it1 = it2
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
it1_._x_=_it2_._x
let x be set ; ::_thesis: ( x in the carrier of L implies it1 . x = it2 . x )
assume x in the carrier of L ; ::_thesis: it1 . x = it2 . x
then reconsider x9 = x as Element of L ;
thus it1 . x = inf (Class ((EqRel R),x9)) by A14
.= it2 . x by A15 ; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines kernel_op WAYBEL20:def_3_:_
for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b3 being kernel Function of L,L holds
( b3 = kernel_op R iff for x being Element of L holds b3 . x = inf (Class ((EqRel R),x)) );
theorem Th36: :: WAYBEL20:36
for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
proof
let L be complete LATTICE; ::_thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
let R be non empty Subset of [:L,L:]; ::_thesis: ( R is CLCongruence implies ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) )
set k = kernel_op R;
set cL = the carrier of L;
A1: dom (kernel_op R) = the carrier of L by FUNCT_2:def_1;
assume A2: R is CLCongruence ; ::_thesis: ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
then A3: R is Equivalence_Relation of the carrier of L by Def2;
then A4: EqRel R = R by Def1;
A5: subrelstr R is CLSubFrame of [:L,L:] by A2, Def2;
thus kernel_op R is directed-sups-preserving ::_thesis: R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L)
proof
let D be Subset of L; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or kernel_op R preserves_sup_of D )
assume that
A6: ( not D is empty & D is directed ) and
ex_sup_of D,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (kernel_op R) .: D,L & "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L)) )
consider e being set such that
A7: e in D by A6, XBOOLE_0:def_1;
set S = { [((kernel_op R) . x),x] where x is Element of L : x in D } ;
A8: { [((kernel_op R) . x),x] where x is Element of L : x in D } c= R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [((kernel_op R) . x),x] where x is Element of L : x in D } or x in R )
assume x in { [((kernel_op R) . x),x] where x is Element of L : x in D } ; ::_thesis: x in R
then consider a being Element of L such that
A9: x = [((kernel_op R) . a),a] and
a in D ;
(kernel_op R) . a = inf (Class ((EqRel R),a)) by A2, Def3;
hence x in R by A2, A9, Th35; ::_thesis: verum
end;
then reconsider S9 = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of (subrelstr R) by YELLOW_0:def_15;
reconsider S = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of [:L,L:] by A8, XBOOLE_1:1;
thus ex_sup_of (kernel_op R) .: D,L by YELLOW_0:17; ::_thesis: "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L))
set d = sup D;
set ds = sup ((kernel_op R) .: D);
A10: ( the carrier of (subrelstr R) = R & ex_sup_of S,[:L,L:] ) by YELLOW_0:17, YELLOW_0:def_15;
reconsider e = e as Element of L by A7;
A11: [((kernel_op R) . e),e] in S by A7;
A12: S9 is directed
proof
let x, y be Element of (subrelstr R); :: according to WAYBEL_0:def_1 ::_thesis: ( not x in S9 or not y in S9 or ex b1 being Element of the carrier of (subrelstr R) st
( b1 in S9 & x <= b1 & y <= b1 ) )
assume that
A13: x in S9 and
A14: y in S9 ; ::_thesis: ex b1 being Element of the carrier of (subrelstr R) st
( b1 in S9 & x <= b1 & y <= b1 )
consider a being Element of L such that
A15: x = [((kernel_op R) . a),a] and
A16: a in D by A13;
consider b being Element of L such that
A17: y = [((kernel_op R) . b),b] and
A18: b in D by A14;
consider c being Element of L such that
A19: c in D and
A20: a <= c and
A21: b <= c by A6, A16, A18, WAYBEL_0:def_1;
set z = [((kernel_op R) . c),c];
[((kernel_op R) . c),c] in S9 by A19;
then reconsider z = [((kernel_op R) . c),c] as Element of (subrelstr R) ;
take z ; ::_thesis: ( z in S9 & x <= z & y <= z )
thus z in S9 by A19; ::_thesis: ( x <= z & y <= z )
(kernel_op R) . a <= (kernel_op R) . c by A20, WAYBEL_1:def_2;
then [((kernel_op R) . a),a] <= [((kernel_op R) . c),c] by A20, YELLOW_3:11;
hence x <= z by A15, YELLOW_0:60; ::_thesis: y <= z
(kernel_op R) . b <= (kernel_op R) . c by A21, WAYBEL_1:def_2;
then [((kernel_op R) . b),b] <= [((kernel_op R) . c),c] by A21, YELLOW_3:11;
hence y <= z by A17, YELLOW_0:60; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_proj1_S_implies_x_in_(kernel_op_R)_.:_D_)_&_(_x_in_(kernel_op_R)_.:_D_implies_x_in_proj1_S_)_)
let x be set ; ::_thesis: ( ( x in proj1 S implies x in (kernel_op R) .: D ) & ( x in (kernel_op R) .: D implies x in proj1 S ) )
hereby ::_thesis: ( x in (kernel_op R) .: D implies x in proj1 S )
assume x in proj1 S ; ::_thesis: x in (kernel_op R) .: D
then consider y being set such that
A22: [x,y] in S by XTUPLE_0:def_12;
consider a being Element of L such that
A23: [x,y] = [((kernel_op R) . a),a] and
A24: a in D by A22;
x = (kernel_op R) . a by A23, XTUPLE_0:1;
hence x in (kernel_op R) .: D by A1, A24, FUNCT_1:def_6; ::_thesis: verum
end;
assume x in (kernel_op R) .: D ; ::_thesis: x in proj1 S
then consider y being set such that
A25: y in dom (kernel_op R) and
A26: y in D and
A27: x = (kernel_op R) . y by FUNCT_1:def_6;
reconsider y = y as Element of L by A25;
[((kernel_op R) . y),y] in S by A26;
hence x in proj1 S by A27, XTUPLE_0:def_12; ::_thesis: verum
end;
then A28: proj1 S = (kernel_op R) .: D by TARSKI:1;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_proj2_S_implies_x_in_D_)_&_(_x_in_D_implies_x_in_proj2_S_)_)
let x be set ; ::_thesis: ( ( x in proj2 S implies x in D ) & ( x in D implies x in proj2 S ) )
hereby ::_thesis: ( x in D implies x in proj2 S )
assume x in proj2 S ; ::_thesis: x in D
then consider y being set such that
A29: [y,x] in S by XTUPLE_0:def_13;
ex a being Element of L st
( [y,x] = [((kernel_op R) . a),a] & a in D ) by A29;
hence x in D by XTUPLE_0:1; ::_thesis: verum
end;
assume A30: x in D ; ::_thesis: x in proj2 S
then reconsider x9 = x as Element of L ;
[((kernel_op R) . x9),x9] in S by A30;
hence x in proj2 S by XTUPLE_0:def_13; ::_thesis: verum
end;
then proj2 S = D by TARSKI:1;
then sup S = [(sup ((kernel_op R) .: D)),(sup D)] by A28, Th8, YELLOW_0:17;
then [(sup ((kernel_op R) .: D)),(sup D)] in R by A5, A10, A11, A12, WAYBEL_0:def_4;
then A31: sup ((kernel_op R) .: D) in Class ((EqRel R),(sup D)) by A4, EQREL_1:19;
(kernel_op R) .: D is_<=_than (kernel_op R) . (sup D)
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in (kernel_op R) .: D or b <= (kernel_op R) . (sup D) )
assume b in (kernel_op R) .: D ; ::_thesis: b <= (kernel_op R) . (sup D)
then consider a being set such that
A32: a in dom (kernel_op R) and
A33: a in D and
A34: b = (kernel_op R) . a by FUNCT_1:def_6;
reconsider a = a as Element of L by A32;
D is_<=_than sup D by YELLOW_0:32;
then a <= sup D by A33, LATTICE3:def_9;
hence b <= (kernel_op R) . (sup D) by A34, WAYBEL_1:def_2; ::_thesis: verum
end;
then A35: sup ((kernel_op R) .: D) <= (kernel_op R) . (sup D) by YELLOW_0:32;
(kernel_op R) . (sup D) = inf (Class ((EqRel R),(sup D))) by A2, Def3;
then (kernel_op R) . (sup D) <= sup ((kernel_op R) .: D) by A31, YELLOW_2:22;
hence "\/" (((kernel_op R) .: D),L) = (kernel_op R) . ("\/" (D,L)) by A35, YELLOW_0:def_3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_R_implies_x_in_[:(kernel_op_R),(kernel_op_R):]_"_(id_the_carrier_of_L)_)_&_(_x_in_[:(kernel_op_R),(kernel_op_R):]_"_(id_the_carrier_of_L)_implies_x_in_R_)_)
let x be set ; ::_thesis: ( ( x in R implies x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) & ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R ) )
hereby ::_thesis: ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R )
assume A36: x in R ; ::_thesis: x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L)
then x in the carrier of [:L,L:] ;
then x in [: the carrier of L, the carrier of L:] by YELLOW_3:def_2;
then consider x1, x2 being set such that
A37: ( x1 in the carrier of L & x2 in the carrier of L ) and
A38: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x1 = x1, x2 = x2 as Element of L by A37;
A39: ( (kernel_op R) . x1 = inf (Class ((EqRel R),x1)) & (kernel_op R) . x2 = inf (Class ((EqRel R),x2)) ) by A2, Def3;
x1 in Class ((EqRel R),x2) by A4, A36, A38, EQREL_1:19;
then (kernel_op R) . x1 = (kernel_op R) . x2 by A39, EQREL_1:23;
then A40: [((kernel_op R) . x1),((kernel_op R) . x2)] in id the carrier of L by RELAT_1:def_10;
dom [:(kernel_op R),(kernel_op R):] = [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def_8;
then A41: [x1,x2] in dom [:(kernel_op R),(kernel_op R):] by A1, ZFMISC_1:87;
[:(kernel_op R),(kernel_op R):] . (x1,x2) = [((kernel_op R) . x1),((kernel_op R) . x2)] by A1, FUNCT_3:def_8;
hence x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by A38, A40, A41, FUNCT_1:def_7; ::_thesis: verum
end;
assume A42: x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ; ::_thesis: x in R
then A43: [:(kernel_op R),(kernel_op R):] . x in id the carrier of L by FUNCT_1:def_7;
x in dom [:(kernel_op R),(kernel_op R):] by A42, FUNCT_1:def_7;
then x in [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def_8;
then consider x1, x2 being set such that
A44: ( x1 in dom (kernel_op R) & x2 in dom (kernel_op R) ) and
A45: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x1 = x1, x2 = x2 as Element of L by A44;
[:(kernel_op R),(kernel_op R):] . (x1,x2) = [((kernel_op R) . x1),((kernel_op R) . x2)] by A44, FUNCT_3:def_8;
then A46: (kernel_op R) . x1 = (kernel_op R) . x2 by A43, A45, RELAT_1:def_10;
(kernel_op R) . x1 = inf (Class ((EqRel R),x1)) by A2, Def3;
then [((kernel_op R) . x1),x1] in R by A2, Th35;
then A47: [x1,((kernel_op R) . x1)] in R by A3, EQREL_1:6;
(kernel_op R) . x2 = inf (Class ((EqRel R),x2)) by A2, Def3;
then [((kernel_op R) . x2),x2] in R by A2, Th35;
hence x in R by A3, A45, A46, A47, EQREL_1:7; ::_thesis: verum
end;
hence R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by TARSKI:1; ::_thesis: verum
end;
theorem Th37: :: WAYBEL20:37
for L being complete continuous LATTICE
for R being Subset of [:L,L:]
for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
proof
let L be complete continuous LATTICE; ::_thesis: for R being Subset of [:L,L:]
for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
let R be Subset of [:L,L:]; ::_thesis: for k being kernel Function of L,L st k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) holds
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
let k be kernel Function of L,L; ::_thesis: ( k is directed-sups-preserving & R = [:k,k:] " (id the carrier of L) implies ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) )
assume that
A1: k is directed-sups-preserving and
A2: R = [:k,k:] " (id the carrier of L) ; ::_thesis: ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
set ER = EqRel R;
R is Equivalence_Relation of the carrier of L by A2, Th2;
then A3: EqRel R = R by Def1;
reconsider rngk = rng k as non empty set ;
defpred S1[ set , set ] means ex x, y being Element of L st
( $1 = Class ((EqRel R),x) & $2 = Class ((EqRel R),y) & k . x <= k . y );
set xx = the Element of L;
set cL = the carrier of L;
Class ((EqRel R), the Element of L) in Class (EqRel R) by EQREL_1:def_3;
then reconsider CER = Class (EqRel R) as non empty Subset-Family of the carrier of L ;
consider LR being non empty strict RelStr such that
A4: the carrier of LR = CER and
A5: for a, b being Element of LR holds
( a <= b iff S1[a,b] ) from YELLOW_0:sch_1();
defpred S2[ set , set ] means ex a being Element of the carrier of L st
( $1 = Class ((EqRel R),a) & $2 = k . a );
A6: dom k = the carrier of L by FUNCT_2:def_1;
A7: for x being Element of CER ex y being Element of rngk st S2[x,y]
proof
let x be Element of CER; ::_thesis: ex y being Element of rngk st S2[x,y]
consider y being set such that
A8: y in the carrier of L and
A9: x = Class ((EqRel R),y) by EQREL_1:def_3;
reconsider y = y as Element of L by A8;
reconsider ky = k . y as Element of rngk by A6, FUNCT_1:def_3;
take ky ; ::_thesis: S2[x,ky]
thus S2[x,ky] by A9; ::_thesis: verum
end;
consider f being Function of CER,rngk such that
A10: for x being Element of CER holds S2[x,f . x] from FUNCT_2:sch_3(A7);
A11: dom [:k,k:] = [: the carrier of L, the carrier of L:] by A6, FUNCT_3:def_8;
A12: for a, b being Element of the carrier of L holds
( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b )
proof
let a, b be Element of the carrier of L; ::_thesis: ( Class ((EqRel R),a) = Class ((EqRel R),b) iff k . a = k . b )
hereby ::_thesis: ( k . a = k . b implies Class ((EqRel R),a) = Class ((EqRel R),b) )
assume Class ((EqRel R),a) = Class ((EqRel R),b) ; ::_thesis: k . a = k . b
then a in Class ((EqRel R),b) by EQREL_1:23;
then [a,b] in R by A3, EQREL_1:19;
then [:k,k:] . (a,b) in id the carrier of L by A2, FUNCT_1:def_7;
then [(k . a),(k . b)] in id the carrier of L by A6, FUNCT_3:def_8;
hence k . a = k . b by RELAT_1:def_10; ::_thesis: verum
end;
assume k . a = k . b ; ::_thesis: Class ((EqRel R),a) = Class ((EqRel R),b)
then [(k . a),(k . b)] in id the carrier of L by RELAT_1:def_10;
then ( [a,b] in [: the carrier of L, the carrier of L:] & [:k,k:] . (a,b) in id the carrier of L ) by A6, FUNCT_3:def_8, ZFMISC_1:def_2;
then [a,b] in EqRel R by A2, A3, A11, FUNCT_1:def_7;
then a in Class ((EqRel R),b) by EQREL_1:19;
hence Class ((EqRel R),a) = Class ((EqRel R),b) by EQREL_1:23; ::_thesis: verum
end;
A13: for x being Element of L holds f . (Class ((EqRel R),x)) = k . x
proof
let x be Element of L; ::_thesis: f . (Class ((EqRel R),x)) = k . x
reconsider CERx = Class ((EqRel R),x) as Element of CER by EQREL_1:def_3;
ex a being Element of the carrier of L st
( CERx = Class ((EqRel R),a) & f . CERx = k . a ) by A10;
hence f . (Class ((EqRel R),x)) = k . x by A12; ::_thesis: verum
end;
A14: for x being Element of LR ex a being Element of L st x = Class ((EqRel R),a)
proof
let x be Element of LR; ::_thesis: ex a being Element of L st x = Class ((EqRel R),a)
x in CER by A4;
then consider a being set such that
A15: a in the carrier of L and
A16: x = Class ((EqRel R),a) by EQREL_1:def_3;
reconsider a = a as Element of L by A15;
take a ; ::_thesis: x = Class ((EqRel R),a)
thus x = Class ((EqRel R),a) by A16; ::_thesis: verum
end;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_CER_&_x2_in_CER_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in CER & x2 in CER & f . x1 = f . x2 implies x1 = x2 )
assume that
A17: x1 in CER and
A18: x2 in CER and
A19: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider x19 = x1 as Element of LR by A4, A17;
consider a being Element of L such that
A20: x19 = Class ((EqRel R),a) by A14;
reconsider x29 = x2 as Element of LR by A4, A18;
consider b being Element of L such that
A21: x29 = Class ((EqRel R),b) by A14;
A22: f . x29 = k . b by A13, A21;
f . x19 = k . a by A13, A20;
hence x1 = x2 by A12, A19, A20, A21, A22; ::_thesis: verum
end;
then A23: f is one-to-one by FUNCT_2:19;
set tIR = the InternalRel of LR;
A24: dom f = CER by FUNCT_2:def_1;
reconsider f = f as Function of LR,(Image k) by A4, YELLOW_0:def_15;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_rng_f_implies_y_in_rngk_)_&_(_y_in_rngk_implies_y_in_rng_f_)_)
let y be set ; ::_thesis: ( ( y in rng f implies y in rngk ) & ( y in rngk implies y in rng f ) )
hereby ::_thesis: ( y in rngk implies y in rng f )
assume y in rng f ; ::_thesis: y in rngk
then consider x being set such that
A25: x in dom f and
A26: y = f . x by FUNCT_1:def_3;
reconsider x = x as Element of LR by A25;
consider a being Element of L such that
A27: x = Class ((EqRel R),a) by A14;
f . x = k . a by A13, A27;
hence y in rngk by A6, A26, FUNCT_1:def_3; ::_thesis: verum
end;
assume y in rngk ; ::_thesis: y in rng f
then consider x being set such that
A28: x in dom k and
A29: y = k . x by FUNCT_1:def_3;
reconsider x = x as Element of L by A28;
( Class ((EqRel R),x) in CER & f . (Class ((EqRel R),x)) = k . x ) by A13, EQREL_1:def_3;
hence y in rng f by A24, A29, FUNCT_1:def_3; ::_thesis: verum
end;
then A30: ( the carrier of (Image k) = rngk & rng f = rngk ) by TARSKI:1, YELLOW_0:def_15;
for x, y being Element of LR holds
( x <= y iff f . x <= f . y )
proof
let x, y be Element of LR; ::_thesis: ( x <= y iff f . x <= f . y )
x in CER by A4;
then consider a being set such that
A31: a in the carrier of L and
A32: x = Class ((EqRel R),a) by EQREL_1:def_3;
hereby ::_thesis: ( f . x <= f . y implies x <= y )
assume x <= y ; ::_thesis: f . x <= f . y
then consider c, d being Element of L such that
A33: ( x = Class ((EqRel R),c) & y = Class ((EqRel R),d) ) and
A34: k . c <= k . d by A5;
( f . x = k . c & f . y = k . d ) by A13, A33;
hence f . x <= f . y by A34, YELLOW_0:60; ::_thesis: verum
end;
reconsider a = a as Element of L by A31;
assume A35: f . x <= f . y ; ::_thesis: x <= y
y in CER by A4;
then consider b being set such that
A36: b in the carrier of L and
A37: y = Class ((EqRel R),b) by EQREL_1:def_3;
reconsider b = b as Element of L by A36;
A38: f . y = k . b by A13, A37;
f . x = k . a by A13, A32;
then k . a <= k . b by A38, A35, YELLOW_0:59;
hence x <= y by A5, A32, A37; ::_thesis: verum
end;
then A39: f is isomorphic by A23, A30, WAYBEL_0:66;
then A40: LR, Image k are_isomorphic by WAYBEL_1:def_8;
then Image k,LR are_isomorphic by WAYBEL_1:6;
then reconsider LR = LR as non empty strict Poset by Th15, Th16, Th17;
Image k is complete by WAYBEL_1:54;
then reconsider LR = LR as non empty strict complete Poset by A40, Th18, WAYBEL_1:6;
reconsider LR = LR as strict complete LATTICE ;
Image k is continuous LATTICE by A1, WAYBEL15:14;
then reconsider LR = LR as strict complete continuous LATTICE by A40, WAYBEL15:9, WAYBEL_1:6;
reconsider f9 = f " as Function of (Image k),LR by A23, A30, FUNCT_2:25;
set IR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ;
A41: f9 is isomorphic by A39, WAYBEL_0:68;
then A42: ( corestr k is infs-preserving & f9 is infs-preserving ) by WAYBEL13:20, WAYBEL_1:56;
take LR ; ::_thesis: ( the carrier of LR = Class (EqRel R) & the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
thus the carrier of LR = Class (EqRel R) by A4; ::_thesis: ( the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) )
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_the_InternalRel_of_LR_implies_z_in__{__[(Class_((EqRel_R),x)),(Class_((EqRel_R),y))]_where_x,_y_is_Element_of_L_:_k_._x_<=_k_._y__}__)_&_(_z_in__{__[(Class_((EqRel_R),x)),(Class_((EqRel_R),y))]_where_x,_y_is_Element_of_L_:_k_._x_<=_k_._y__}__implies_z_in_the_InternalRel_of_LR_)_)
let z be set ; ::_thesis: ( ( z in the InternalRel of LR implies z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ) & ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR ) )
hereby ::_thesis: ( z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } implies z in the InternalRel of LR )
assume A43: z in the InternalRel of LR ; ::_thesis: z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y }
then consider a, b being set such that
A44: ( a in CER & b in CER ) and
A45: z = [a,b] by A4, ZFMISC_1:def_2;
reconsider a = a, b = b as Element of LR by A4, A44;
a <= b by A43, A45, ORDERS_2:def_5;
then ex x, y being Element of L st
( a = Class ((EqRel R),x) & b = Class ((EqRel R),y) & k . x <= k . y ) by A5;
hence z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } by A45; ::_thesis: verum
end;
assume z in { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } ; ::_thesis: z in the InternalRel of LR
then consider x, y being Element of L such that
A46: z = [(Class ((EqRel R),x)),(Class ((EqRel R),y))] and
A47: k . x <= k . y ;
reconsider b = Class ((EqRel R),y) as Element of LR by A4, EQREL_1:def_3;
reconsider a = Class ((EqRel R),x) as Element of LR by A4, EQREL_1:def_3;
a <= b by A5, A47;
hence z in the InternalRel of LR by A46, ORDERS_2:def_5; ::_thesis: verum
end;
hence the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } by TARSKI:1; ::_thesis: for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR
let g be Function of L,LR; ::_thesis: ( ( for x being Element of L holds g . x = Class ((EqRel R),x) ) implies g is CLHomomorphism of L,LR )
assume A48: for x being Element of L holds g . x = Class ((EqRel R),x) ; ::_thesis: g is CLHomomorphism of L,LR
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
(f9_*_(corestr_k))_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of L implies (f9 * (corestr k)) . x = g . x )
assume A49: x in the carrier of L ; ::_thesis: (f9 * (corestr k)) . x = g . x
then reconsider x9 = x as Element of L ;
A50: ( f . (Class ((EqRel R),x9)) = k . x9 & Class ((EqRel R),x9) in CER ) by A13, EQREL_1:def_3;
dom (corestr k) = the carrier of L by FUNCT_2:def_1;
hence (f9 * (corestr k)) . x = f9 . ((corestr k) . x) by A49, FUNCT_1:13
.= f9 . (k . x) by WAYBEL_1:30
.= Class ((EqRel R),x9) by A24, A23, A50, FUNCT_1:32
.= g . x by A48 ;
::_thesis: verum
end;
then A51: g = f9 * (corestr k) by FUNCT_2:12;
A52: corestr k is directed-sups-preserving by A1, Th22;
reconsider f9 = f9 as sups-preserving Function of (Image k),LR by A41, WAYBEL13:20;
f9 is directed-sups-preserving ;
then A53: g is directed-sups-preserving by A51, A52, WAYBEL15:11;
g is infs-preserving by A51, A42, Th25;
hence g is CLHomomorphism of L,LR by A53, WAYBEL16:def_1; ::_thesis: verum
end;
theorem Th38: :: WAYBEL20:38
for L being complete continuous LATTICE
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) holds
subrelstr R is CLSubFrame of [:L,L:]
proof
let L be complete continuous LATTICE; ::_thesis: for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) holds
subrelstr R is CLSubFrame of [:L,L:]
let R be Subset of [:L,L:]; ::_thesis: ( R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) implies subrelstr R is CLSubFrame of [:L,L:] )
assume R is Equivalence_Relation of the carrier of L ; ::_thesis: ( for LR being complete continuous LATTICE holds
( not the carrier of LR = Class (EqRel R) or ex g being Function of L,LR st
( ( for x being Element of L holds g . x = Class ((EqRel R),x) ) & g is not CLHomomorphism of L,LR ) ) or subrelstr R is CLSubFrame of [:L,L:] )
then A1: EqRel R = R by Def1;
set ER = EqRel R;
given LR being complete continuous LATTICE such that A2: the carrier of LR = Class (EqRel R) and
A3: for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ; ::_thesis: subrelstr R is CLSubFrame of [:L,L:]
deffunc H1( set ) -> Element of bool the carrier of L = Class ((EqRel R),$1);
set CER = Class (EqRel R);
set cL = the carrier of L;
set cLR = the carrier of LR;
A4: for x being set st x in the carrier of L holds
H1(x) in Class (EqRel R) by EQREL_1:def_3;
consider g being Function of the carrier of L,(Class (EqRel R)) such that
A5: for x being set st x in the carrier of L holds
g . x = H1(x) from FUNCT_2:sch_2(A4);
reconsider g = g as Function of L,LR by A2;
set k = g;
A6: dom g = the carrier of L by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_R_implies_x_in_[:g,g:]_"_(id_the_carrier_of_LR)_)_&_(_x_in_[:g,g:]_"_(id_the_carrier_of_LR)_implies_x_in_R_)_)
let x be set ; ::_thesis: ( ( x in R implies x in [:g,g:] " (id the carrier of LR) ) & ( x in [:g,g:] " (id the carrier of LR) implies x in R ) )
hereby ::_thesis: ( x in [:g,g:] " (id the carrier of LR) implies x in R )
assume A7: x in R ; ::_thesis: x in [:g,g:] " (id the carrier of LR)
then x in the carrier of [:L,L:] ;
then x in [: the carrier of L, the carrier of L:] by YELLOW_3:def_2;
then consider x1, x2 being set such that
A8: ( x1 in the carrier of L & x2 in the carrier of L ) and
A9: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x1 = x1, x2 = x2 as Element of L by A8;
A10: ( g . x1 = Class ((EqRel R),x1) & g . x2 = Class ((EqRel R),x2) ) by A5;
x1 in Class ((EqRel R),x2) by A1, A7, A9, EQREL_1:19;
then g . x1 = g . x2 by A10, EQREL_1:23;
then A11: [(g . x1),(g . x2)] in id the carrier of LR by RELAT_1:def_10;
dom [:g,g:] = [:(dom g),(dom g):] by FUNCT_3:def_8;
then A12: [x1,x2] in dom [:g,g:] by A6, ZFMISC_1:87;
[:g,g:] . (x1,x2) = [(g . x1),(g . x2)] by A6, FUNCT_3:def_8;
hence x in [:g,g:] " (id the carrier of LR) by A9, A11, A12, FUNCT_1:def_7; ::_thesis: verum
end;
assume A13: x in [:g,g:] " (id the carrier of LR) ; ::_thesis: x in R
then A14: [:g,g:] . x in id the carrier of LR by FUNCT_1:def_7;
x in dom [:g,g:] by A13, FUNCT_1:def_7;
then x in [:(dom g),(dom g):] by FUNCT_3:def_8;
then consider x1, x2 being set such that
A15: ( x1 in dom g & x2 in dom g ) and
A16: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x1 = x1, x2 = x2 as Element of L by A15;
A17: ( g . x1 = Class ((EqRel R),x1) & g . x2 = Class ((EqRel R),x2) ) by A5;
[:g,g:] . (x1,x2) = [(g . x1),(g . x2)] by A15, FUNCT_3:def_8;
then g . x1 = g . x2 by A14, A16, RELAT_1:def_10;
then x1 in Class ((EqRel R),x2) by A17, EQREL_1:23;
hence x in R by A1, A16, EQREL_1:19; ::_thesis: verum
end;
then A18: R = [:g,g:] " (id the carrier of LR) by TARSKI:1;
for x being Element of L holds g . x = Class ((EqRel R),x) by A5;
then g is CLHomomorphism of L,LR by A3;
hence subrelstr R is CLSubFrame of [:L,L:] by A18, Th34; ::_thesis: verum
end;
registration
let L be non empty reflexive RelStr ;
cluster non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like V17( the carrier of L) V25( the carrier of L, the carrier of L) directed-sups-preserving kernel for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being Function of L,L st
( b1 is directed-sups-preserving & b1 is kernel )
proof
reconsider k = id L as directed-sups-preserving kernel Function of L,L ;
take k ; ::_thesis: ( k is directed-sups-preserving & k is kernel )
thus ( k is directed-sups-preserving & k is kernel ) ; ::_thesis: verum
end;
end;
definition
let L be non empty reflexive RelStr ;
let k be kernel Function of L,L;
func kernel_congruence k -> non empty Subset of [:L,L:] equals :: WAYBEL20:def 4
[:k,k:] " (id the carrier of L);
coherence
[:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:]
proof
set cL = the carrier of L;
set x = the Element of the carrier of L;
A1: dom k = the carrier of L by FUNCT_2:def_1;
then A2: ( [(k . the Element of the carrier of L),(k . the Element of the carrier of L)] in id the carrier of L & [:k,k:] . ( the Element of the carrier of L, the Element of the carrier of L) = [(k . the Element of the carrier of L),(k . the Element of the carrier of L)] ) by FUNCT_3:def_8, RELAT_1:def_10;
dom [:k,k:] = [:(dom k),(dom k):] by FUNCT_3:def_8;
then [ the Element of the carrier of L, the Element of the carrier of L] in dom [:k,k:] by A1, ZFMISC_1:def_2;
hence [:k,k:] " (id the carrier of L) is non empty Subset of [:L,L:] by A2, FUNCT_1:def_7; ::_thesis: verum
end;
end;
:: deftheorem defines kernel_congruence WAYBEL20:def_4_:_
for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k = [:k,k:] " (id the carrier of L);
theorem :: WAYBEL20:39
for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k is Equivalence_Relation of the carrier of L by Th2;
theorem Th40: :: WAYBEL20:40
for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence
proof
let L be complete continuous LATTICE; ::_thesis: for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence
let k be directed-sups-preserving kernel Function of L,L; ::_thesis: kernel_congruence k is CLCongruence
set R = kernel_congruence k;
thus A1: kernel_congruence k is Equivalence_Relation of the carrier of L by Th2; :: according to WAYBEL20:def_2 ::_thesis: subrelstr (kernel_congruence k) is CLSubFrame of [:L,L:]
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel (kernel_congruence k)) & the InternalRel of LR = { [(Class ((EqRel (kernel_congruence k)),x)),(Class ((EqRel (kernel_congruence k)),y))] where x, y is Element of L : k . x <= k . y } & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel (kernel_congruence k)),x) ) holds
g is CLHomomorphism of L,LR ) ) by Th37;
hence subrelstr (kernel_congruence k) is CLSubFrame of [:L,L:] by A1, Th38; ::_thesis: verum
end;
definition
let L be complete continuous LATTICE;
let R be non empty Subset of [:L,L:];
assume B1: R is CLCongruence ;
funcL ./. R -> strict complete continuous LATTICE means :Def5: :: WAYBEL20:def 5
( the carrier of it = Class (EqRel R) & ( for x, y being Element of it holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) );
existence
ex b1 being strict complete continuous LATTICE st
( the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) )
proof
set k = kernel_op R;
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) by B1, Th36;
then consider LR being strict complete continuous LATTICE such that
A1: the carrier of LR = Class (EqRel R) and
A2: the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : (kernel_op R) . x <= (kernel_op R) . y } and
for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR by Th37;
take LR ; ::_thesis: ( the carrier of LR = Class (EqRel R) & ( for x, y being Element of LR holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) )
thus the carrier of LR = Class (EqRel R) by A1; ::_thesis: for x, y being Element of LR holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) )
let x, y be Element of LR; ::_thesis: ( x <= y iff "/\" (x,L) <= "/\" (y,L) )
x in the carrier of LR ;
then consider u being set such that
A3: u in the carrier of L and
A4: x = Class ((EqRel R),u) by A1, EQREL_1:def_3;
y in the carrier of LR ;
then consider v being set such that
A5: v in the carrier of L and
A6: y = Class ((EqRel R),v) by A1, EQREL_1:def_3;
hereby ::_thesis: ( "/\" (x,L) <= "/\" (y,L) implies x <= y )
assume x <= y ; ::_thesis: "/\" (x,L) <= "/\" (y,L)
then [x,y] in the InternalRel of LR by ORDERS_2:def_5;
then consider u9, v9 being Element of L such that
A7: [x,y] = [(Class ((EqRel R),u9)),(Class ((EqRel R),v9))] and
A8: (kernel_op R) . u9 <= (kernel_op R) . v9 by A2;
A9: ( x = Class ((EqRel R),u9) & y = Class ((EqRel R),v9) ) by A7, XTUPLE_0:1;
(kernel_op R) . u9 = inf (Class ((EqRel R),u9)) by B1, Def3;
hence "/\" (x,L) <= "/\" (y,L) by B1, A8, A9, Def3; ::_thesis: verum
end;
assume A10: "/\" (x,L) <= "/\" (y,L) ; ::_thesis: x <= y
reconsider u = u, v = v as Element of L by A3, A5;
( (kernel_op R) . u = inf (Class ((EqRel R),u)) & (kernel_op R) . v = inf (Class ((EqRel R),v)) ) by B1, Def3;
then [x,y] in the InternalRel of LR by A2, A4, A6, A10;
hence x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict complete continuous LATTICE st the carrier of b1 = Class (EqRel R) & ( for x, y being Element of b1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of b2 = Class (EqRel R) & ( for x, y being Element of b2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) holds
b1 = b2
proof
let LR1, LR2 be strict complete continuous LATTICE; ::_thesis: ( the carrier of LR1 = Class (EqRel R) & ( for x, y being Element of LR1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) & the carrier of LR2 = Class (EqRel R) & ( for x, y being Element of LR2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) implies LR1 = LR2 )
assume that
A11: the carrier of LR1 = Class (EqRel R) and
A12: for x, y being Element of LR1 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) and
A13: the carrier of LR2 = Class (EqRel R) and
A14: for x, y being Element of LR2 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ; ::_thesis: LR1 = LR2
set cLR2 = the carrier of LR2;
set cLR1 = the carrier of LR1;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_the_InternalRel_of_LR1_implies_z_in_the_InternalRel_of_LR2_)_&_(_z_in_the_InternalRel_of_LR2_implies_z_in_the_InternalRel_of_LR1_)_)
let z be set ; ::_thesis: ( ( z in the InternalRel of LR1 implies z in the InternalRel of LR2 ) & ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 ) )
hereby ::_thesis: ( z in the InternalRel of LR2 implies z in the InternalRel of LR1 )
assume A15: z in the InternalRel of LR1 ; ::_thesis: z in the InternalRel of LR2
then consider x, y being set such that
A16: ( x in the carrier of LR1 & y in the carrier of LR1 ) and
A17: z = [x,y] by ZFMISC_1:def_2;
reconsider x = x, y = y as Element of LR1 by A16;
reconsider x9 = x, y9 = y as Element of LR2 by A11, A13;
x <= y by A15, A17, ORDERS_2:def_5;
then "/\" (x,L) <= "/\" (y,L) by A12;
then x9 <= y9 by A14;
hence z in the InternalRel of LR2 by A17, ORDERS_2:def_5; ::_thesis: verum
end;
assume A18: z in the InternalRel of LR2 ; ::_thesis: z in the InternalRel of LR1
then consider x, y being set such that
A19: ( x in the carrier of LR2 & y in the carrier of LR2 ) and
A20: z = [x,y] by ZFMISC_1:def_2;
reconsider x = x, y = y as Element of LR2 by A19;
reconsider x9 = x, y9 = y as Element of LR1 by A11, A13;
x <= y by A18, A20, ORDERS_2:def_5;
then "/\" (x,L) <= "/\" (y,L) by A14;
then x9 <= y9 by A12;
hence z in the InternalRel of LR1 by A20, ORDERS_2:def_5; ::_thesis: verum
end;
hence LR1 = LR2 by A11, A13, TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines ./. WAYBEL20:def_5_:_
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b3 being strict complete continuous LATTICE holds
( b3 = L ./. R iff ( the carrier of b3 = Class (EqRel R) & ( for x, y being Element of b3 holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) );
theorem :: WAYBEL20:41
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) )
proof
let L be complete continuous LATTICE; ::_thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) )
let R be non empty Subset of [:L,L:]; ::_thesis: ( R is CLCongruence implies for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) ) )
assume R is CLCongruence ; ::_thesis: for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) )
then A1: the carrier of (L ./. R) = Class (EqRel R) by Def5;
let x be set ; ::_thesis: ( x is Element of (L ./. R) iff ex y being Element of L st x = Class ((EqRel R),y) )
hereby ::_thesis: ( ex y being Element of L st x = Class ((EqRel R),y) implies x is Element of (L ./. R) )
assume x is Element of (L ./. R) ; ::_thesis: ex y being Element of L st x = Class ((EqRel R),y)
then x in Class (EqRel R) by A1;
then consider y being set such that
A2: y in the carrier of L and
A3: x = Class ((EqRel R),y) by EQREL_1:def_3;
reconsider y = y as Element of L by A2;
take y = y; ::_thesis: x = Class ((EqRel R),y)
thus x = Class ((EqRel R),y) by A3; ::_thesis: verum
end;
given y being Element of L such that A4: x = Class ((EqRel R),y) ; ::_thesis: x is Element of (L ./. R)
thus x is Element of (L ./. R) by A1, A4, EQREL_1:def_3; ::_thesis: verum
end;
theorem :: WAYBEL20:42
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
R = kernel_congruence (kernel_op R) by Th36;
theorem :: WAYBEL20:43
for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)
proof
let L be complete continuous LATTICE; ::_thesis: for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)
let k be directed-sups-preserving kernel Function of L,L; ::_thesis: k = kernel_op (kernel_congruence k)
set kc = kernel_congruence k;
set cL = the carrier of L;
set km = kernel_op (kernel_congruence k);
A1: dom k = the carrier of L by FUNCT_2:def_1;
A2: kernel_op (kernel_congruence k) <= id L by WAYBEL_1:def_15;
A3: k <= id L by WAYBEL_1:def_15;
A4: kernel_congruence k is CLCongruence by Th40;
then A5: kernel_congruence k = [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] " (id the carrier of L) by Th36;
reconsider kc9 = kernel_congruence k as Equivalence_Relation of the carrier of L by A4, Def2;
field kc9 = the carrier of L by ORDERS_1:12;
then A6: kc9 is_transitive_in the carrier of L by RELAT_2:def_16;
A7: dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] = [:(dom (kernel_op (kernel_congruence k))),(dom (kernel_op (kernel_congruence k))):] by FUNCT_3:def_8;
A8: dom (kernel_op (kernel_congruence k)) = the carrier of L by FUNCT_2:def_1;
A9: dom [:k,k:] = [:(dom k),(dom k):] by FUNCT_3:def_8;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
k_._x_=_(kernel_op_(kernel_congruence_k))_._x
let x be set ; ::_thesis: ( x in the carrier of L implies k . x = (kernel_op (kernel_congruence k)) . x )
assume x in the carrier of L ; ::_thesis: k . x = (kernel_op (kernel_congruence k)) . x
then reconsider x9 = x as Element of L ;
A10: k . (k . x9) = (k * k) . x9 by A1, FUNCT_1:13
.= k . x9 by QUANTAL1:def_9 ;
A11: ( [(k . x9),(k . x9)] in id the carrier of L & [:k,k:] . ((k . x9),x9) = [(k . (k . x9)),(k . x9)] ) by A1, FUNCT_3:def_8, RELAT_1:def_10;
[(k . x9),x9] in dom [:k,k:] by A1, A9, ZFMISC_1:def_2;
then A12: [(k . x9),x9] in kernel_congruence k by A10, A11, FUNCT_1:def_7;
A13: (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9) = ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9 by A8, FUNCT_1:13
.= (kernel_op (kernel_congruence k)) . x9 by QUANTAL1:def_9 ;
(kernel_op (kernel_congruence k)) . (k . x9) <= (id L) . (k . x9) by A2, YELLOW_2:9;
then A14: (kernel_op (kernel_congruence k)) . (k . x9) <= k . x9 by FUNCT_1:18;
A15: ( [((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . x9)] in id the carrier of L & [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . (x9,((kernel_op (kernel_congruence k)) . x9)) = [((kernel_op (kernel_congruence k)) . x9),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] ) by A8, FUNCT_3:def_8, RELAT_1:def_10;
[x9,((kernel_op (kernel_congruence k)) . x9)] in dom [:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] by A8, A7, ZFMISC_1:def_2;
then [x9,((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k by A5, A13, A15, FUNCT_1:def_7;
then A16: [(k . x9),((kernel_op (kernel_congruence k)) . x9)] in kernel_congruence k by A6, A12, RELAT_2:def_8;
then [:k,k:] . ((k . x9),((kernel_op (kernel_congruence k)) . x9)) in id the carrier of L by FUNCT_1:def_7;
then [(k . (k . x9)),(k . ((kernel_op (kernel_congruence k)) . x9))] in id the carrier of L by A1, FUNCT_3:def_8;
then A17: k . ((kernel_op (kernel_congruence k)) . x9) = k . (k . x9) by RELAT_1:def_10
.= (k * k) . x9 by A1, FUNCT_1:13
.= k . x9 by QUANTAL1:def_9 ;
[:(kernel_op (kernel_congruence k)),(kernel_op (kernel_congruence k)):] . ((k . x9),((kernel_op (kernel_congruence k)) . x9)) in id the carrier of L by A5, A16, FUNCT_1:def_7;
then [((kernel_op (kernel_congruence k)) . (k . x9)),((kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9))] in id the carrier of L by A8, FUNCT_3:def_8;
then A18: (kernel_op (kernel_congruence k)) . (k . x9) = (kernel_op (kernel_congruence k)) . ((kernel_op (kernel_congruence k)) . x9) by RELAT_1:def_10
.= ((kernel_op (kernel_congruence k)) * (kernel_op (kernel_congruence k))) . x9 by A8, FUNCT_1:13
.= (kernel_op (kernel_congruence k)) . x9 by QUANTAL1:def_9 ;
k . ((kernel_op (kernel_congruence k)) . x9) <= (id L) . ((kernel_op (kernel_congruence k)) . x9) by A3, YELLOW_2:9;
then k . ((kernel_op (kernel_congruence k)) . x9) <= (kernel_op (kernel_congruence k)) . x9 by FUNCT_1:18;
hence k . x = (kernel_op (kernel_congruence k)) . x by A17, A18, A14, YELLOW_0:def_3; ::_thesis: verum
end;
hence k = kernel_op (kernel_congruence k) by FUNCT_2:12; ::_thesis: verum
end;
theorem :: WAYBEL20:44
for L being complete continuous LATTICE
for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )
proof
let L be complete continuous LATTICE; ::_thesis: for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )
let p be projection Function of L,L; ::_thesis: ( p is infs-preserving implies ( Image p is continuous LATTICE & Image p is infs-inheriting ) )
assume A1: p is infs-preserving ; ::_thesis: ( Image p is continuous LATTICE & Image p is infs-inheriting )
reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by WAYBEL_1:43;
reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by WAYBEL_1:45;
A2: subrelstr Lc is infs-inheriting by A1, WAYBEL_1:51;
then A3: subrelstr Lc is complete by YELLOW_2:30;
A4: pc is infs-preserving
proof
let X be Subset of (subrelstr Lc); :: according to WAYBEL_0:def_32 ::_thesis: pc preserves_inf_of X
assume ex_inf_of X, subrelstr Lc ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of pc .: X, subrelstr Lc & "/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc))) )
thus ex_inf_of pc .: X, subrelstr Lc by A3, YELLOW_0:17; ::_thesis: "/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc)))
the carrier of (subrelstr Lc) = Lc by YELLOW_0:def_15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
A5: ( ex_inf_of X9,L & p preserves_inf_of X9 ) by A1, WAYBEL_0:def_32, YELLOW_0:17;
X c= the carrier of (subrelstr Lc) ;
then X c= Lc by YELLOW_0:def_15;
then A6: pc .: X = p .: X by RELAT_1:129;
A7: ex_inf_of X,L by YELLOW_0:17;
then "/\" (X9,L) in the carrier of (subrelstr Lc) by A2, YELLOW_0:def_18;
then A8: ( dom pc = the carrier of (subrelstr Lc) & inf X9 = inf X ) by A7, FUNCT_2:def_1, YELLOW_0:63;
( ex_inf_of p .: X,L & "/\" ((pc .: X),L) in the carrier of (subrelstr Lc) ) by A2, YELLOW_0:17, YELLOW_0:def_18;
hence inf (pc .: X) = inf (p .: X) by A6, YELLOW_0:63
.= p . (inf X9) by A5, WAYBEL_0:def_30
.= pc . (inf X) by A8, FUNCT_1:47 ;
::_thesis: verum
end;
reconsider cpc = corestr pc as Function of (subrelstr Lc),(Image pc) ;
A9: the carrier of (subrelstr (rng p)) = rng p by YELLOW_0:def_15
.= rng pc by WAYBEL_1:44
.= the carrier of (subrelstr (rng pc)) by YELLOW_0:def_15 ;
subrelstr (rng pc) is full SubRelStr of L by WAYBEL15:1;
then A10: Image p = Image pc by A9, YELLOW_0:57;
pc is closure by WAYBEL_1:47;
then A11: cpc is sups-preserving by WAYBEL_1:55;
subrelstr Lc is sups-inheriting SubRelStr of L by WAYBEL_1:49;
then subrelstr Lc is continuous LATTICE by A2, WAYBEL_5:28;
hence Image p is continuous LATTICE by A3, A10, A4, A11, Th19, WAYBEL_5:33; ::_thesis: Image p is infs-inheriting
thus Image p is infs-inheriting by A1, A2, WAYBEL_1:51; ::_thesis: verum
end;