:: WAYBEL13 semantic presentation
begin
theorem Th1: :: WAYBEL13:1
for L being non empty reflexive transitive RelStr
for x, y being Element of L st x <= y holds
compactbelow x c= compactbelow y
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds
compactbelow x c= compactbelow y
let x, y be Element of L; ::_thesis: ( x <= y implies compactbelow x c= compactbelow y )
assume A1: x <= y ; ::_thesis: compactbelow x c= compactbelow y
now__::_thesis:_for_z_being_set_st_z_in_compactbelow_x_holds_
z_in_compactbelow_y
let z be set ; ::_thesis: ( z in compactbelow x implies z in compactbelow y )
assume z in compactbelow x ; ::_thesis: z in compactbelow y
then z in { v where v is Element of L : ( x >= v & v is compact ) } by WAYBEL_8:def_2;
then consider z9 being Element of L such that
A2: z9 = z and
A3: x >= z9 and
A4: z9 is compact ;
z9 <= y by A1, A3, ORDERS_2:3;
hence z in compactbelow y by A2, A4, WAYBEL_8:4; ::_thesis: verum
end;
hence compactbelow x c= compactbelow y by TARSKI:def_3; ::_thesis: verum
end;
theorem Th2: :: WAYBEL13:2
for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x is Subset of (CompactSublatt L)
proof
let L be non empty reflexive RelStr ; ::_thesis: for x being Element of L holds compactbelow x is Subset of (CompactSublatt L)
let x be Element of L; ::_thesis: compactbelow x is Subset of (CompactSublatt L)
now__::_thesis:_for_v_being_set_st_v_in_compactbelow_x_holds_
v_in_the_carrier_of_(CompactSublatt_L)
let v be set ; ::_thesis: ( v in compactbelow x implies v in the carrier of (CompactSublatt L) )
assume v in compactbelow x ; ::_thesis: v in the carrier of (CompactSublatt L)
then v in { z where z is Element of L : ( x >= z & z is compact ) } by WAYBEL_8:def_2;
then ex v1 being Element of L st
( v1 = v & x >= v1 & v1 is compact ) ;
hence v in the carrier of (CompactSublatt L) by WAYBEL_8:def_1; ::_thesis: verum
end;
hence compactbelow x is Subset of (CompactSublatt L) by TARSKI:def_3; ::_thesis: verum
end;
theorem Th3: :: WAYBEL13:3
for L being RelStr
for S being SubRelStr of L
for X being Subset of S holds X is Subset of L
proof
let L be RelStr ; ::_thesis: for S being SubRelStr of L
for X being Subset of S holds X is Subset of L
let S be SubRelStr of L; ::_thesis: for X being Subset of S holds X is Subset of L
let X be Subset of S; ::_thesis: X is Subset of L
the carrier of S c= the carrier of L by YELLOW_0:def_13;
hence X is Subset of L by XBOOLE_1:1; ::_thesis: verum
end;
theorem Th4: :: WAYBEL13:4
for L being non empty reflexive transitive with_suprema RelStr holds the carrier of L is Ideal of L
proof
let L be non empty reflexive transitive with_suprema RelStr ; ::_thesis: the carrier of L is Ideal of L
[#] L is Ideal of L ;
hence the carrier of L is Ideal of L ; ::_thesis: verum
end;
theorem Th5: :: WAYBEL13:5
for L1 being non empty reflexive antisymmetric lower-bounded RelStr
for L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)
proof
let L1 be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: for L2 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete holds
the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)
let L2 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is up-complete implies the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: L1 is up-complete ; ::_thesis: the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2)
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(CompactSublatt_L2)_holds_
x_in_the_carrier_of_(CompactSublatt_L1)
reconsider L29 = L2 as non empty reflexive antisymmetric lower-bounded RelStr by A1, YELLOW_0:13;
let x be set ; ::_thesis: ( x in the carrier of (CompactSublatt L2) implies x in the carrier of (CompactSublatt L1) )
assume A3: x in the carrier of (CompactSublatt L2) ; ::_thesis: x in the carrier of (CompactSublatt L1)
then x is Element of (CompactSublatt L29) ;
then reconsider x2 = x as Element of L2 by YELLOW_0:58;
reconsider x1 = x2 as Element of L1 by A1;
A4: x2 is compact by A3, WAYBEL_8:def_1;
L2 is up-complete by A1, A2, WAYBEL_8:15;
then x1 is compact by A1, A4, WAYBEL_8:9;
hence x in the carrier of (CompactSublatt L1) by WAYBEL_8:def_1; ::_thesis: verum
end;
then A5: the carrier of (CompactSublatt L2) c= the carrier of (CompactSublatt L1) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(CompactSublatt_L1)_holds_
x_in_the_carrier_of_(CompactSublatt_L2)
let x be set ; ::_thesis: ( x in the carrier of (CompactSublatt L1) implies x in the carrier of (CompactSublatt L2) )
assume A6: x in the carrier of (CompactSublatt L1) ; ::_thesis: x in the carrier of (CompactSublatt L2)
then reconsider x1 = x as Element of L1 by YELLOW_0:58;
reconsider x2 = x1 as Element of L2 by A1;
x1 is compact by A6, WAYBEL_8:def_1;
then x2 is compact by A1, A2, WAYBEL_8:9;
hence x in the carrier of (CompactSublatt L2) by WAYBEL_8:def_1; ::_thesis: verum
end;
then the carrier of (CompactSublatt L1) c= the carrier of (CompactSublatt L2) by TARSKI:def_3;
hence the carrier of (CompactSublatt L1) = the carrier of (CompactSublatt L2) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem Th6: :: WAYBEL13:6
for L being lower-bounded algebraic LATTICE
for S being CLSubFrame of L holds S is algebraic
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: for S being CLSubFrame of L holds S is algebraic
let S be CLSubFrame of L; ::_thesis: S is algebraic
RelStr(# the carrier of S, the InternalRel of S #) = Image (closure_op S) by WAYBEL10:18;
then RelStr(# the carrier of S, the InternalRel of S #) is algebraic by WAYBEL_8:24;
hence S is algebraic by WAYBEL_8:17; ::_thesis: verum
end;
theorem Th7: :: WAYBEL13:7
for X, E being set
for L being CLSubFrame of BoolePoset X holds
( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )
proof
let X, E be set ; ::_thesis: for L being CLSubFrame of BoolePoset X holds
( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )
let L be CLSubFrame of BoolePoset X; ::_thesis: ( E in the carrier of (CompactSublatt L) iff ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) )
A1: the carrier of L c= the carrier of (BoolePoset X) by YELLOW_0:def_13;
A2: L is complete LATTICE by YELLOW_2:30;
thus ( E in the carrier of (CompactSublatt L) implies ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) ) ::_thesis: ( ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) implies E in the carrier of (CompactSublatt L) )
proof
A3: (closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) = [#] (CompactSublatt (Image (closure_op L))) by WAYBEL_8:25
.= [#] (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) by WAYBEL10:18
.= the carrier of (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) ;
assume E in the carrier of (CompactSublatt L) ; ::_thesis: ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E )
then E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) by A2, A3, Th5;
then consider x being set such that
A4: x in dom (closure_op L) and
A5: x in [#] (CompactSublatt (BoolePoset X)) and
A6: E = (closure_op L) . x by FUNCT_1:def_6;
reconsider F = x as Element of (BoolePoset X) by A4;
id (BoolePoset X) <= closure_op L by WAYBEL_1:def_14;
then (id (BoolePoset X)) . F <= (closure_op L) . F by YELLOW_2:9;
then F <= (closure_op L) . F by FUNCT_1:18;
then A7: F c= (closure_op L) . F by YELLOW_1:2;
(closure_op L) . x in rng (closure_op L) by A4, FUNCT_1:def_3;
then (closure_op L) . x in the carrier of (Image (closure_op L)) by YELLOW_0:def_15;
then (closure_op L) . x in the carrier of RelStr(# the carrier of L, the InternalRel of L #) by WAYBEL10:18;
then A8: (closure_op L) . x in { Y where Y is Element of L : F c= Y } by A7;
take F ; ::_thesis: ( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E )
F is compact by A5, WAYBEL_8:def_1;
hence F is finite by WAYBEL_8:28; ::_thesis: ( E = meet { Y where Y is Element of L : F c= Y } & F c= E )
A9: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (uparrow F) /\ the carrier of L or z in { Y where Y is Element of L : F c= Y } )
assume A10: z in (uparrow F) /\ the carrier of L ; ::_thesis: z in { Y where Y is Element of L : F c= Y }
then reconsider z9 = z as Element of (BoolePoset X) ;
z in uparrow F by A10, XBOOLE_0:def_4;
then F <= z9 by WAYBEL_0:18;
then A11: F c= z by YELLOW_1:2;
z in the carrier of L by A10, XBOOLE_0:def_4;
hence z in { Y where Y is Element of L : F c= Y } by A11; ::_thesis: verum
end;
{ Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { Y where Y is Element of L : F c= Y } or z in (uparrow F) /\ the carrier of L )
assume z in { Y where Y is Element of L : F c= Y } ; ::_thesis: z in (uparrow F) /\ the carrier of L
then consider z9 being Element of L such that
A12: z = z9 and
A13: F c= z9 ;
reconsider z1 = z9 as Element of (BoolePoset X) by A1, TARSKI:def_3;
F <= z1 by A13, YELLOW_1:2;
then z in uparrow F by A12, WAYBEL_0:18;
hence z in (uparrow F) /\ the carrier of L by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
then A14: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c= Y } by A9, XBOOLE_0:def_10;
thus A15: E = "/\" (((uparrow F) /\ the carrier of L),(BoolePoset X)) by A6, WAYBEL10:def_5
.= meet { Y where Y is Element of L : F c= Y } by A8, A14, YELLOW_1:20 ; ::_thesis: F c= E
now__::_thesis:_for_v_being_set_st_v_in_F_holds_
v_in_E
let v be set ; ::_thesis: ( v in F implies v in E )
assume A16: v in F ; ::_thesis: v in E
now__::_thesis:_for_V_being_set_st_V_in__{__Y_where_Y_is_Element_of_L_:_F_c=_Y__}__holds_
v_in_V
let V be set ; ::_thesis: ( V in { Y where Y is Element of L : F c= Y } implies v in V )
assume V in { Y where Y is Element of L : F c= Y } ; ::_thesis: v in V
then ex V9 being Element of L st
( V = V9 & F c= V9 ) ;
hence v in V by A16; ::_thesis: verum
end;
hence v in E by A8, A15, SETFAM_1:def_1; ::_thesis: verum
end;
hence F c= E by TARSKI:def_3; ::_thesis: verum
end;
thus ( ex F being Element of (BoolePoset X) st
( F is finite & E = meet { Y where Y is Element of L : F c= Y } & F c= E ) implies E in the carrier of (CompactSublatt L) ) ::_thesis: verum
proof
given F being Element of (BoolePoset X) such that A17: F is finite and
A18: E = meet { Y where Y is Element of L : F c= Y } and
F c= E ; ::_thesis: E in the carrier of (CompactSublatt L)
F is compact by A17, WAYBEL_8:28;
then A19: F in [#] (CompactSublatt (BoolePoset X)) by WAYBEL_8:def_1;
A20: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (uparrow F) /\ the carrier of L or z in { Y where Y is Element of L : F c= Y } )
assume A21: z in (uparrow F) /\ the carrier of L ; ::_thesis: z in { Y where Y is Element of L : F c= Y }
then reconsider z9 = z as Element of (BoolePoset X) ;
z in uparrow F by A21, XBOOLE_0:def_4;
then F <= z9 by WAYBEL_0:18;
then A22: F c= z by YELLOW_1:2;
z in the carrier of L by A21, XBOOLE_0:def_4;
hence z in { Y where Y is Element of L : F c= Y } by A22; ::_thesis: verum
end;
{ Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { Y where Y is Element of L : F c= Y } or z in (uparrow F) /\ the carrier of L )
assume z in { Y where Y is Element of L : F c= Y } ; ::_thesis: z in (uparrow F) /\ the carrier of L
then consider z9 being Element of L such that
A23: z = z9 and
A24: F c= z9 ;
reconsider z1 = z9 as Element of (BoolePoset X) by A1, TARSKI:def_3;
F <= z1 by A24, YELLOW_1:2;
then z in uparrow F by A23, WAYBEL_0:18;
hence z in (uparrow F) /\ the carrier of L by A23, XBOOLE_0:def_4; ::_thesis: verum
end;
then A25: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c= Y } by A20, XBOOLE_0:def_10;
id (BoolePoset X) <= closure_op L by WAYBEL_1:def_14;
then (id (BoolePoset X)) . F <= (closure_op L) . F by YELLOW_2:9;
then F <= (closure_op L) . F by FUNCT_1:18;
then A26: F c= (closure_op L) . F by YELLOW_1:2;
F in the carrier of (BoolePoset X) ;
then A27: F in dom (closure_op L) by FUNCT_2:def_1;
then (closure_op L) . F in rng (closure_op L) by FUNCT_1:def_3;
then (closure_op L) . F in the carrier of (Image (closure_op L)) by YELLOW_0:def_15;
then (closure_op L) . F in the carrier of RelStr(# the carrier of L, the InternalRel of L #) by WAYBEL10:18;
then (closure_op L) . F in { Y where Y is Element of L : F c= Y } by A26;
then E = "/\" (((uparrow F) /\ the carrier of L),(BoolePoset X)) by A18, A25, YELLOW_1:20
.= (closure_op L) . F by WAYBEL10:def_5 ;
then A28: E in (closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) by A27, A19, FUNCT_1:def_6;
(closure_op L) .: ([#] (CompactSublatt (BoolePoset X))) = [#] (CompactSublatt (Image (closure_op L))) by WAYBEL_8:25
.= [#] (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) by WAYBEL10:18
.= the carrier of (CompactSublatt RelStr(# the carrier of L, the InternalRel of L #)) ;
hence E in the carrier of (CompactSublatt L) by A2, A28, Th5; ::_thesis: verum
end;
end;
theorem Th8: :: WAYBEL13:8
for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L
now__::_thesis:_for_x_being_set_st_x_in_Ids_L_holds_
x_in_bool_the_carrier_of_L
let x be set ; ::_thesis: ( x in Ids L implies x in bool the carrier of L )
assume x in Ids L ; ::_thesis: x in bool the carrier of L
then x in { X where X is Ideal of L : verum } by WAYBEL_0:def_23;
then ex x9 being Ideal of L st x9 = x ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then Ids L is Subset-Family of L by TARSKI:def_3;
then reconsider InIdL = InclPoset (Ids L) as non empty full SubRelStr of BoolePoset the carrier of L by YELLOW_1:5;
A1: for X being directed Subset of InIdL st X <> {} & ex_sup_of X, BoolePoset the carrier of L holds
"\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL
proof
let X be directed Subset of InIdL; ::_thesis: ( X <> {} & ex_sup_of X, BoolePoset the carrier of L implies "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL )
assume that
A2: X <> {} and
ex_sup_of X, BoolePoset the carrier of L ; ::_thesis: "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL
consider Y being set such that
A3: Y in X by A2, XBOOLE_0:def_1;
X is Subset of (BoolePoset the carrier of L) by Th3;
then A4: "\/" (X,(BoolePoset the carrier of L)) = union X by YELLOW_1:21;
then reconsider uX = union X as Subset of L by WAYBEL_8:26;
Y is Ideal of L by A3, YELLOW_2:41;
then Bottom L in Y by WAYBEL_4:21;
then reconsider uX = uX as non empty Subset of L by A3, TARSKI:def_4;
now__::_thesis:_for_z_being_set_st_z_in_X_holds_
z_in_bool_the_carrier_of_L
let z be set ; ::_thesis: ( z in X implies z in bool the carrier of L )
assume z in X ; ::_thesis: z in bool the carrier of L
then z is Ideal of L by YELLOW_2:41;
hence z in bool the carrier of L ; ::_thesis: verum
end;
then A5: X c= bool the carrier of L by TARSKI:def_3;
A6: now__::_thesis:_for_Y,_Z_being_Subset_of_L_st_Y_in_X_&_Z_in_X_holds_
ex_V_being_Subset_of_L_st_
(_V_in_X_&_Y_\/_Z_c=_V_)
let Y, Z be Subset of L; ::_thesis: ( Y in X & Z in X implies ex V being Subset of L st
( V in X & Y \/ Z c= V ) )
assume A7: ( Y in X & Z in X ) ; ::_thesis: ex V being Subset of L st
( V in X & Y \/ Z c= V )
then reconsider Y9 = Y, Z9 = Z as Element of InIdL ;
consider V9 being Element of InIdL such that
A8: V9 in X and
A9: ( Y9 <= V9 & Z9 <= V9 ) by A7, WAYBEL_0:def_1;
reconsider V = V9 as Subset of L by YELLOW_2:41;
take V = V; ::_thesis: ( V in X & Y \/ Z c= V )
thus V in X by A8; ::_thesis: Y \/ Z c= V
Y9 "\/" Z9 <= V9 by A9, YELLOW_0:22;
then A10: Y9 "\/" Z9 c= V9 by YELLOW_1:3;
Y \/ Z c= Y9 "\/" Z9 by YELLOW_1:6;
hence Y \/ Z c= V by A10, XBOOLE_1:1; ::_thesis: verum
end;
( ( for Y being Subset of L st Y in X holds
Y is lower ) & ( for Y being Subset of L st Y in X holds
Y is directed ) ) by YELLOW_2:41;
then uX is Ideal of L by A5, A6, WAYBEL_0:26, WAYBEL_0:46;
then "\/" (X,(BoolePoset the carrier of L)) is Element of InIdL by A4, YELLOW_2:41;
hence "\/" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum
end;
for X being Subset of InIdL st ex_inf_of X, BoolePoset the carrier of L holds
"/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL
proof
let X be Subset of InIdL; ::_thesis: ( ex_inf_of X, BoolePoset the carrier of L implies "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL )
assume ex_inf_of X, BoolePoset the carrier of L ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL
now__::_thesis:_"/\"_(X,(BoolePoset_the_carrier_of_L))_in_the_carrier_of_InIdL
percases ( not X is empty or X is empty ) ;
supposeA11: not X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL
X is Subset of (BoolePoset the carrier of L) by Th3;
then A12: "/\" (X,(BoolePoset the carrier of L)) = meet X by A11, YELLOW_1:20;
InclPoset (Ids L) = RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1;
then "/\" (X,(BoolePoset the carrier of L)) is Ideal of L by A11, A12, YELLOW_2:45;
then "/\" (X,(BoolePoset the carrier of L)) is Element of InIdL by YELLOW_2:41;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum
end;
supposeA13: X is empty ; ::_thesis: "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL
"/\" ({},(BoolePoset the carrier of L)) = Top (BoolePoset the carrier of L) by YELLOW_0:def_12
.= the carrier of L by YELLOW_1:19 ;
then "/\" ({},(BoolePoset the carrier of L)) is Ideal of L by Th4;
then "/\" (X,(BoolePoset the carrier of L)) is Element of InIdL by A13, YELLOW_2:41;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum
end;
end;
end;
hence "/\" (X,(BoolePoset the carrier of L)) in the carrier of InIdL ; ::_thesis: verum
end;
hence InclPoset (Ids L) is CLSubFrame of BoolePoset the carrier of L by A1, WAYBEL_0:def_4, YELLOW_0:def_18; ::_thesis: verum
end;
registration
let L be non empty reflexive transitive RelStr ;
cluster non empty directed lower principal for Element of K32( the carrier of L);
existence
ex b1 being Ideal of L st b1 is principal
proof
set x = the Element of L;
take downarrow the Element of L ; ::_thesis: downarrow the Element of L is principal
thus downarrow the Element of L is principal by WAYBEL_0:48; ::_thesis: verum
end;
end;
theorem Th9: :: WAYBEL13:9
for L being lower-bounded sup-Semilattice
for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for X being non empty directed Subset of (InclPoset (Ids L)) holds sup X = union X
let X be non empty directed Subset of (InclPoset (Ids L)); ::_thesis: sup X = union X
consider z being set such that
A1: z in X by XBOOLE_0:def_1;
X c= the carrier of (InclPoset (Ids L)) ;
then A2: X c= Ids L by YELLOW_1:1;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_in_bool_the_carrier_of_L
let x be set ; ::_thesis: ( x in X implies x in bool the carrier of L )
assume x in X ; ::_thesis: x in bool the carrier of L
then x in Ids L by A2;
then x in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23;
then ex x1 being Ideal of L st x = x1 ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then A3: X c= bool the carrier of L by TARSKI:def_3;
now__::_thesis:_for_Z_being_Subset_of_L_st_Z_in_X_holds_
Z_is_lower
let Z be Subset of L; ::_thesis: ( Z in X implies Z is lower )
assume Z in X ; ::_thesis: Z is lower
then Z in Ids L by A2;
then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23;
then ex Z1 being Ideal of L st Z = Z1 ;
hence Z is lower ; ::_thesis: verum
end;
then reconsider unX = union X as lower Subset of L by A3, WAYBEL_0:26;
z in Ids L by A2, A1;
then z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23;
then ex z1 being Ideal of L st z = z1 ;
then ex v being set st v in z by XBOOLE_0:def_1;
then reconsider unX = unX as non empty lower Subset of L by A1, TARSKI:def_4;
A4: now__::_thesis:_for_V,_Y_being_Subset_of_L_st_V_in_X_&_Y_in_X_holds_
ex_Z_being_Subset_of_L_st_
(_Z_in_X_&_V_\/_Y_c=_Z_)
let V, Y be Subset of L; ::_thesis: ( V in X & Y in X implies ex Z being Subset of L st
( Z in X & V \/ Y c= Z ) )
assume A5: ( V in X & Y in X ) ; ::_thesis: ex Z being Subset of L st
( Z in X & V \/ Y c= Z )
then reconsider V1 = V, Y1 = Y as Element of (InclPoset (Ids L)) ;
consider Z1 being Element of (InclPoset (Ids L)) such that
A6: Z1 in X and
A7: ( V1 <= Z1 & Y1 <= Z1 ) by A5, WAYBEL_0:def_1;
Z1 in Ids L by A2, A6;
then Z1 in { Y9 where Y9 is Ideal of L : verum } by WAYBEL_0:def_23;
then ex Z2 being Ideal of L st Z1 = Z2 ;
then reconsider Z = Z1 as Subset of L ;
take Z = Z; ::_thesis: ( Z in X & V \/ Y c= Z )
thus Z in X by A6; ::_thesis: V \/ Y c= Z
( V c= Z & Y c= Z ) by A7, YELLOW_1:3;
hence V \/ Y c= Z by XBOOLE_1:8; ::_thesis: verum
end;
now__::_thesis:_for_Z_being_Subset_of_L_st_Z_in_X_holds_
Z_is_directed
let Z be Subset of L; ::_thesis: ( Z in X implies Z is directed )
assume Z in X ; ::_thesis: Z is directed
then Z in Ids L by A2;
then Z in { Y where Y is Ideal of L : verum } by WAYBEL_0:def_23;
then ex Z1 being Ideal of L st Z = Z1 ;
hence Z is directed ; ::_thesis: verum
end;
then reconsider unX = unX as non empty directed lower Subset of L by A3, A4, WAYBEL_0:46;
reconsider unX = unX as Element of (InclPoset (Ids L)) by YELLOW_2:41;
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
Y_c=_sup_X
let Y be set ; ::_thesis: ( Y in X implies Y c= sup X )
assume A8: Y in X ; ::_thesis: Y c= sup X
then reconsider Y9 = Y as Element of (InclPoset (Ids L)) ;
sup X is_>=_than X by YELLOW_0:32;
then Y9 <= sup X by A8, LATTICE3:def_9;
hence Y c= sup X by YELLOW_1:3; ::_thesis: verum
end;
then union X c= sup X by ZFMISC_1:76;
then A9: unX <= sup X by YELLOW_1:3;
now__::_thesis:_for_b_being_Element_of_(InclPoset_(Ids_L))_st_b_in_X_holds_
b_<=_unX
let b be Element of (InclPoset (Ids L)); ::_thesis: ( b in X implies b <= unX )
assume b in X ; ::_thesis: b <= unX
then b c= union X by ZFMISC_1:74;
hence b <= unX by YELLOW_1:3; ::_thesis: verum
end;
then unX is_>=_than X by LATTICE3:def_9;
then sup X <= unX by YELLOW_0:32;
hence sup X = union X by A9, ORDERS_2:2; ::_thesis: verum
end;
theorem Th10: :: WAYBEL13:10
for S being lower-bounded sup-Semilattice holds InclPoset (Ids S) is algebraic
proof
let S be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids S) is algebraic
set BS = BoolePoset the carrier of S;
Ids S c= bool the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ids S or x in bool the carrier of S )
assume x in Ids S ; ::_thesis: x in bool the carrier of S
then x in { X where X is Ideal of S : verum } by WAYBEL_0:def_23;
then ex x1 being Ideal of S st x = x1 ;
hence x in bool the carrier of S ; ::_thesis: verum
end;
then reconsider InIdsS = InclPoset (Ids S) as non empty full SubRelStr of BoolePoset the carrier of S by YELLOW_1:5;
A1: the carrier of InIdsS c= the carrier of (BoolePoset the carrier of S) by YELLOW_0:def_13;
now__::_thesis:_for_X_being_Subset_of_InIdsS_st_ex_inf_of_X,_BoolePoset_the_carrier_of_S_holds_
"/\"_(X,(BoolePoset_the_carrier_of_S))_in_the_carrier_of_InIdsS
let X be Subset of InIdsS; ::_thesis: ( ex_inf_of X, BoolePoset the carrier of S implies "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS )
assume ex_inf_of X, BoolePoset the carrier of S ; ::_thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS
now__::_thesis:_"/\"_(X,(BoolePoset_the_carrier_of_S))_in_the_carrier_of_InIdsS
percases ( X <> {} or X = {} ) ;
supposeA2: X <> {} ; ::_thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_in_the_carrier_of_(BoolePoset_the_carrier_of_S)
let x be set ; ::_thesis: ( x in X implies x in the carrier of (BoolePoset the carrier of S) )
assume x in X ; ::_thesis: x in the carrier of (BoolePoset the carrier of S)
then x in the carrier of InIdsS ;
hence x in the carrier of (BoolePoset the carrier of S) by A1; ::_thesis: verum
end;
then X c= the carrier of (BoolePoset the carrier of S) by TARSKI:def_3;
then "/\" (X,(BoolePoset the carrier of S)) = meet X by A2, YELLOW_1:20
.= "/\" (X,InIdsS) by A2, YELLOW_2:46 ;
hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS ; ::_thesis: verum
end;
supposeA3: X = {} ; ::_thesis: "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS
"/\" ({},(BoolePoset the carrier of S)) = Top (BoolePoset the carrier of S) by YELLOW_0:def_12
.= the carrier of S by YELLOW_1:19
.= [#] S
.= "/\" ({},InIdsS) by YELLOW_2:47 ;
hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS by A3; ::_thesis: verum
end;
end;
end;
hence "/\" (X,(BoolePoset the carrier of S)) in the carrier of InIdsS ; ::_thesis: verum
end;
then A4: InIdsS is infs-inheriting by YELLOW_0:def_18;
now__::_thesis:_for_Y_being_directed_Subset_of_InIdsS_st_Y_<>_{}_&_ex_sup_of_Y,_BoolePoset_the_carrier_of_S_holds_
"\/"_(Y,(BoolePoset_the_carrier_of_S))_in_the_carrier_of_InIdsS
let Y be directed Subset of InIdsS; ::_thesis: ( Y <> {} & ex_sup_of Y, BoolePoset the carrier of S implies "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS )
assume that
A5: Y <> {} and
ex_sup_of Y, BoolePoset the carrier of S ; ::_thesis: "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
x_in_the_carrier_of_(BoolePoset_the_carrier_of_S)
let x be set ; ::_thesis: ( x in Y implies x in the carrier of (BoolePoset the carrier of S) )
assume x in Y ; ::_thesis: x in the carrier of (BoolePoset the carrier of S)
then x in the carrier of InIdsS ;
hence x in the carrier of (BoolePoset the carrier of S) by A1; ::_thesis: verum
end;
then Y c= the carrier of (BoolePoset the carrier of S) by TARSKI:def_3;
then "\/" (Y,(BoolePoset the carrier of S)) = union Y by YELLOW_1:21
.= "\/" (Y,InIdsS) by A5, Th9 ;
hence "\/" (Y,(BoolePoset the carrier of S)) in the carrier of InIdsS ; ::_thesis: verum
end;
then InIdsS is directed-sups-inheriting by WAYBEL_0:def_4;
hence InclPoset (Ids S) is algebraic by A4, Th6; ::_thesis: verum
end;
theorem Th11: :: WAYBEL13:11
for S being lower-bounded sup-Semilattice
for x being Element of (InclPoset (Ids S)) holds
( x is compact iff x is principal Ideal of S )
proof
let S be lower-bounded sup-Semilattice; ::_thesis: for x being Element of (InclPoset (Ids S)) holds
( x is compact iff x is principal Ideal of S )
reconsider InIdS = InclPoset (Ids S) as CLSubFrame of BoolePoset the carrier of S by Th8;
let x be Element of (InclPoset (Ids S)); ::_thesis: ( x is compact iff x is principal Ideal of S )
reconsider x9 = x as Ideal of S by YELLOW_2:41;
thus ( x is compact implies x is principal Ideal of S ) ::_thesis: ( x is principal Ideal of S implies x is compact )
proof
assume x is compact ; ::_thesis: x is principal Ideal of S
then x in the carrier of (CompactSublatt InIdS) by WAYBEL_8:def_1;
then consider F being Element of (BoolePoset the carrier of S) such that
A1: F is finite and
A2: x = meet { Y where Y is Element of InIdS : F c= Y } and
A3: F c= x by Th7;
A4: F c= the carrier of S by WAYBEL_8:26;
ex y being Element of S st
( y in x9 & y is_>=_than x9 )
proof
reconsider F9 = F as Subset of S by WAYBEL_8:26;
reconsider F9 = F9 as Subset of S ;
reconsider y = sup F9 as Element of S ;
take y ; ::_thesis: ( y in x9 & y is_>=_than x9 )
now__::_thesis:_y_in_x9
percases ( F9 <> {} or F9 = {} ) ;
suppose F9 <> {} ; ::_thesis: y in x9
hence y in x9 by A1, A3, WAYBEL_0:42; ::_thesis: verum
end;
suppose F9 = {} ; ::_thesis: y in x9
then y = Bottom S by YELLOW_0:def_11;
hence y in x9 by WAYBEL_4:21; ::_thesis: verum
end;
end;
end;
hence y in x9 ; ::_thesis: y is_>=_than x9
now__::_thesis:_for_b_being_Element_of_S_st_b_in_x9_holds_
b_<=_y
now__::_thesis:_for_u_being_set_st_u_in_F_holds_
u_in_downarrow_y
let u be set ; ::_thesis: ( u in F implies u in downarrow y )
assume A5: u in F ; ::_thesis: u in downarrow y
then reconsider u9 = u as Element of S by A4;
ex_sup_of F9,S by A1, A5, YELLOW_0:54;
then y is_>=_than F by YELLOW_0:30;
then u9 <= y by A5, LATTICE3:def_9;
hence u in downarrow y by WAYBEL_0:17; ::_thesis: verum
end;
then A6: F c= downarrow y by TARSKI:def_3;
let b be Element of S; ::_thesis: ( b in x9 implies b <= y )
assume A7: b in x9 ; ::_thesis: b <= y
downarrow y is Element of InIdS by YELLOW_2:41;
then downarrow y in { Y where Y is Element of InIdS : F c= Y } by A6;
then b in downarrow y by A2, A7, SETFAM_1:def_1;
hence b <= y by WAYBEL_0:17; ::_thesis: verum
end;
hence y is_>=_than x9 by LATTICE3:def_9; ::_thesis: verum
end;
hence x is principal Ideal of S by WAYBEL_0:def_21; ::_thesis: verum
end;
thus ( x is principal Ideal of S implies x is compact ) ::_thesis: verum
proof
assume x is principal Ideal of S ; ::_thesis: x is compact
then consider y being Element of S such that
A8: y in x9 and
A9: y is_>=_than x9 by WAYBEL_0:def_21;
ex F being Element of (BoolePoset the carrier of S) st
( F is finite & F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } )
proof
reconsider F = {y} as Element of (BoolePoset the carrier of S) by WAYBEL_8:26;
take F ; ::_thesis: ( F is finite & F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } )
thus F is finite ; ::_thesis: ( F c= x & x = meet { Y where Y is Element of InIdS : F c= Y } )
for v being set st v in F holds
v in x by A8, TARSKI:def_1;
hence A10: F c= x by TARSKI:def_3; ::_thesis: x = meet { Y where Y is Element of InIdS : F c= Y }
A11: now__::_thesis:_for_z_being_set_holds_
(_(_z_in_x_implies_for_Z_being_set_st_Z_in__{__Y_where_Y_is_Element_of_InIdS_:_F_c=_Y__}__holds_
z_in_Z_)_&_(_(_for_Z_being_set_st_Z_in__{__Y_where_Y_is_Element_of_InIdS_:_F_c=_Y__}__holds_
z_in_Z_)_implies_z_in_x_)_)
let z be set ; ::_thesis: ( ( z in x implies for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) & ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) implies z in x ) )
thus ( z in x implies for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) ::_thesis: ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) implies z in x )
proof
assume A12: z in x ; ::_thesis: for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z
then reconsider z9 = z as Element of S by YELLOW_2:42;
A13: z9 <= y by A9, A12, LATTICE3:def_9;
let Z be set ; ::_thesis: ( Z in { Y where Y is Element of InIdS : F c= Y } implies z in Z )
assume Z in { Y where Y is Element of InIdS : F c= Y } ; ::_thesis: z in Z
then consider Z1 being Element of InIdS such that
A14: ( Z1 = Z & F c= Z1 ) ;
( Z1 is Ideal of S & y in F ) by TARSKI:def_1, YELLOW_2:41;
hence z in Z by A14, A13, WAYBEL_0:def_19; ::_thesis: verum
end;
thus ( ( for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ) implies z in x ) ::_thesis: verum
proof
assume A15: for Z being set st Z in { Y where Y is Element of InIdS : F c= Y } holds
z in Z ; ::_thesis: z in x
x in { Y where Y is Element of InIdS : F c= Y } by A10;
hence z in x by A15; ::_thesis: verum
end;
end;
[#] S is Element of InIdS by YELLOW_2:41;
then [#] S in { Y where Y is Element of InIdS : F c= Y } ;
hence x = meet { Y where Y is Element of InIdS : F c= Y } by A11, SETFAM_1:def_1; ::_thesis: verum
end;
then x in the carrier of (CompactSublatt InIdS) by Th7;
hence x is compact by WAYBEL_8:def_1; ::_thesis: verum
end;
end;
theorem Th12: :: WAYBEL13:12
for S being lower-bounded sup-Semilattice
for x being Element of (InclPoset (Ids S)) holds
( x is compact iff ex a being Element of S st x = downarrow a )
proof
let S be lower-bounded sup-Semilattice; ::_thesis: for x being Element of (InclPoset (Ids S)) holds
( x is compact iff ex a being Element of S st x = downarrow a )
let x be Element of (InclPoset (Ids S)); ::_thesis: ( x is compact iff ex a being Element of S st x = downarrow a )
thus ( x is compact implies ex a being Element of S st x = downarrow a ) ::_thesis: ( ex a being Element of S st x = downarrow a implies x is compact )
proof
assume x is compact ; ::_thesis: ex a being Element of S st x = downarrow a
then x is principal Ideal of S by Th11;
hence ex a being Element of S st x = downarrow a by WAYBEL_0:48; ::_thesis: verum
end;
thus ( ex a being Element of S st x = downarrow a implies x is compact ) ::_thesis: verum
proof
assume ex a being Element of S st x = downarrow a ; ::_thesis: x is compact
then x is principal Ideal of S by WAYBEL_0:48;
hence x is compact by Th11; ::_thesis: verum
end;
end;
theorem :: WAYBEL13:13
for L being lower-bounded sup-Semilattice
for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds
f is isomorphic
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for f being Function of L,(CompactSublatt (InclPoset (Ids L))) st ( for x being Element of L holds f . x = downarrow x ) holds
f is isomorphic
let f be Function of L,(CompactSublatt (InclPoset (Ids L))); ::_thesis: ( ( for x being Element of L holds f . x = downarrow x ) implies f is isomorphic )
assume A1: for x being Element of L holds f . x = downarrow x ; ::_thesis: f is isomorphic
A2: for x, y being Element of L holds
( x <= y iff f . x <= f . y )
proof
let x, y be Element of L; ::_thesis: ( x <= y iff f . x <= f . y )
reconsider fx = f . x as Element of (InclPoset (Ids L)) by YELLOW_0:58;
reconsider fy = f . y as Element of (InclPoset (Ids L)) by YELLOW_0:58;
thus ( x <= y implies f . x <= f . y ) ::_thesis: ( f . x <= f . y implies x <= y )
proof
assume x <= y ; ::_thesis: f . x <= f . y
then downarrow x c= downarrow y by WAYBEL_0:21;
then f . x c= downarrow y by A1;
then fx c= fy by A1;
then fx <= fy by YELLOW_1:3;
hence f . x <= f . y by YELLOW_0:60; ::_thesis: verum
end;
x <= x ;
then A3: x in downarrow x by WAYBEL_0:17;
thus ( f . x <= f . y implies x <= y ) ::_thesis: verum
proof
assume f . x <= f . y ; ::_thesis: x <= y
then fx <= fy by YELLOW_0:59;
then fx c= fy by YELLOW_1:3;
then f . x c= downarrow y by A1;
then downarrow x c= downarrow y by A1;
hence x <= y by A3, WAYBEL_0:17; ::_thesis: verum
end;
end;
now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_(CompactSublatt_(InclPoset_(Ids_L)))_holds_
ex_x9_being_set_st_
(_x9_in_the_carrier_of_L_&_y_=_f_._x9_)
let y be set ; ::_thesis: ( y in the carrier of (CompactSublatt (InclPoset (Ids L))) implies ex x9 being set st
( x9 in the carrier of L & y = f . x9 ) )
assume A4: y in the carrier of (CompactSublatt (InclPoset (Ids L))) ; ::_thesis: ex x9 being set st
( x9 in the carrier of L & y = f . x9 )
the carrier of (CompactSublatt (InclPoset (Ids L))) c= the carrier of (InclPoset (Ids L)) by YELLOW_0:def_13;
then reconsider y9 = y as Element of (InclPoset (Ids L)) by A4;
y9 is compact by A4, WAYBEL_8:def_1;
then consider x being Element of L such that
A5: y9 = downarrow x by Th12;
reconsider x9 = x as set ;
take x9 = x9; ::_thesis: ( x9 in the carrier of L & y = f . x9 )
thus x9 in the carrier of L ; ::_thesis: y = f . x9
thus y = f . x9 by A1, A5; ::_thesis: verum
end;
then A6: rng f = the carrier of (CompactSublatt (InclPoset (Ids L))) by FUNCT_2:10;
now__::_thesis:_for_x,_y_being_Element_of_L_st_f_._x_=_f_._y_holds_
x_=_y
let x, y be Element of L; ::_thesis: ( f . x = f . y implies x = y )
assume f . x = f . y ; ::_thesis: x = y
then f . x = downarrow y by A1;
then downarrow x = downarrow y by A1;
hence x = y by WAYBEL_0:19; ::_thesis: verum
end;
then f is V13() by WAYBEL_1:def_1;
hence f is isomorphic by A6, A2, WAYBEL_0:66; ::_thesis: verum
end;
theorem :: WAYBEL13:14
for S being lower-bounded LATTICE holds InclPoset (Ids S) is arithmetic
proof
let S be lower-bounded LATTICE; ::_thesis: InclPoset (Ids S) is arithmetic
now__::_thesis:_for_x,_y_being_Element_of_(CompactSublatt_(InclPoset_(Ids_S)))_ex_z_being_Element_of_(CompactSublatt_(InclPoset_(Ids_S)))_st_
(_z_<=_x_&_z_<=_y_&_(_for_v_being_Element_of_(CompactSublatt_(InclPoset_(Ids_S)))_st_v_<=_x_&_v_<=_y_holds_
v_<=_z_)_)
let x, y be Element of (CompactSublatt (InclPoset (Ids S))); ::_thesis: ex z being Element of (CompactSublatt (InclPoset (Ids S))) st
( z <= x & z <= y & ( for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds
v <= z ) )
reconsider x1 = x, y1 = y as Element of (InclPoset (Ids S)) by YELLOW_0:58;
x1 is compact by WAYBEL_8:def_1;
then consider a being Element of S such that
A1: x1 = downarrow a by Th12;
y1 is compact by WAYBEL_8:def_1;
then consider b being Element of S such that
A2: y1 = downarrow b by Th12;
Bottom S <= b by YELLOW_0:44;
then A3: Bottom S in downarrow b by WAYBEL_0:17;
Bottom S <= a by YELLOW_0:44;
then Bottom S in downarrow a by WAYBEL_0:17;
then reconsider xy = (downarrow a) /\ (downarrow b) as non empty Subset of S by A3, XBOOLE_0:def_4;
reconsider xy = xy as non empty lower Subset of S by WAYBEL_0:27;
reconsider xy = xy as non empty directed lower Subset of S by WAYBEL_0:44;
xy is Ideal of S ;
then (downarrow a) /\ (downarrow b) in { X where X is Ideal of S : verum } ;
then (downarrow a) /\ (downarrow b) in Ids S by WAYBEL_0:def_23;
then x1 "/\" y1 = (downarrow a) /\ (downarrow b) by A1, A2, YELLOW_1:9;
then reconsider z1 = (downarrow a) /\ (downarrow b) as Element of (InclPoset (Ids S)) ;
z1 c= y1 by A2, XBOOLE_1:17;
then A4: z1 <= y1 by YELLOW_1:3;
A5: downarrow (a "/\" b) c= (downarrow a) /\ (downarrow b)
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in downarrow (a "/\" b) or v in (downarrow a) /\ (downarrow b) )
assume A6: v in downarrow (a "/\" b) ; ::_thesis: v in (downarrow a) /\ (downarrow b)
then reconsider v1 = v as Element of S ;
A7: v1 <= a "/\" b by A6, WAYBEL_0:17;
a "/\" b <= b by YELLOW_0:23;
then v1 <= b by A7, ORDERS_2:3;
then A8: v in downarrow b by WAYBEL_0:17;
a "/\" b <= a by YELLOW_0:23;
then v1 <= a by A7, ORDERS_2:3;
then v in downarrow a by WAYBEL_0:17;
hence v in (downarrow a) /\ (downarrow b) by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
(downarrow a) /\ (downarrow b) c= downarrow (a "/\" b)
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in (downarrow a) /\ (downarrow b) or v in downarrow (a "/\" b) )
assume A9: v in (downarrow a) /\ (downarrow b) ; ::_thesis: v in downarrow (a "/\" b)
then reconsider v1 = v as Element of S ;
v in downarrow b by A9, XBOOLE_0:def_4;
then A10: v1 <= b by WAYBEL_0:17;
v in downarrow a by A9, XBOOLE_0:def_4;
then v1 <= a by WAYBEL_0:17;
then v1 <= a "/\" b by A10, YELLOW_0:23;
hence v in downarrow (a "/\" b) by WAYBEL_0:17; ::_thesis: verum
end;
then z1 = downarrow (a "/\" b) by A5, XBOOLE_0:def_10;
then z1 is compact by Th12;
then reconsider z = z1 as Element of (CompactSublatt (InclPoset (Ids S))) by WAYBEL_8:def_1;
take z = z; ::_thesis: ( z <= x & z <= y & ( for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds
v <= z ) )
z1 c= x1 by A1, XBOOLE_1:17;
then z1 <= x1 by YELLOW_1:3;
hence ( z <= x & z <= y ) by A4, YELLOW_0:60; ::_thesis: for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds
v <= z
let v be Element of (CompactSublatt (InclPoset (Ids S))); ::_thesis: ( v <= x & v <= y implies v <= z )
reconsider v1 = v as Element of (InclPoset (Ids S)) by YELLOW_0:58;
assume that
A11: v <= x and
A12: v <= y ; ::_thesis: v <= z
v1 <= y1 by A12, YELLOW_0:59;
then A13: v1 c= y1 by YELLOW_1:3;
v1 <= x1 by A11, YELLOW_0:59;
then v1 c= x1 by YELLOW_1:3;
then v1 c= z1 by A1, A2, A13, XBOOLE_1:19;
then v1 <= z1 by YELLOW_1:3;
hence v <= z by YELLOW_0:60; ::_thesis: verum
end;
then A14: CompactSublatt (InclPoset (Ids S)) is with_infima by LATTICE3:def_11;
InclPoset (Ids S) is algebraic by Th10;
hence InclPoset (Ids S) is arithmetic by A14, WAYBEL_8:19; ::_thesis: verum
end;
theorem Th15: :: WAYBEL13:15
for L being lower-bounded sup-Semilattice holds CompactSublatt L is lower-bounded sup-Semilattice
proof
let L be lower-bounded sup-Semilattice; ::_thesis: CompactSublatt L is lower-bounded sup-Semilattice
ex x being Element of (CompactSublatt L) st x is_<=_than the carrier of (CompactSublatt L)
proof
reconsider x = Bottom L as Element of (CompactSublatt L) by WAYBEL_8:3;
take x ; ::_thesis: x is_<=_than the carrier of (CompactSublatt L)
now__::_thesis:_for_a_being_Element_of_(CompactSublatt_L)_st_a_in_the_carrier_of_(CompactSublatt_L)_holds_
x_<=_a
let a be Element of (CompactSublatt L); ::_thesis: ( a in the carrier of (CompactSublatt L) implies x <= a )
A1: the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def_13;
assume a in the carrier of (CompactSublatt L) ; ::_thesis: x <= a
then reconsider a9 = a as Element of L by A1;
Bottom L <= a9 by YELLOW_0:44;
hence x <= a by YELLOW_0:60; ::_thesis: verum
end;
hence x is_<=_than the carrier of (CompactSublatt L) by LATTICE3:def_8; ::_thesis: verum
end;
hence CompactSublatt L is lower-bounded sup-Semilattice by YELLOW_0:def_4; ::_thesis: verum
end;
theorem Th16: :: WAYBEL13:16
for L being lower-bounded algebraic sup-Semilattice
for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds
f is isomorphic
proof
let L be lower-bounded algebraic sup-Semilattice; ::_thesis: for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds
f is isomorphic
let f be Function of L,(InclPoset (Ids (CompactSublatt L))); ::_thesis: ( ( for x being Element of L holds f . x = compactbelow x ) implies f is isomorphic )
assume A1: for x being Element of L holds f . x = compactbelow x ; ::_thesis: f is isomorphic
A2: now__::_thesis:_for_x,_y_being_Element_of_L_holds_
(_(_x_<=_y_implies_f_._x_<=_f_._y_)_&_(_f_._x_<=_f_._y_implies_x_<=_y_)_)
let x, y be Element of L; ::_thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
thus ( x <= y implies f . x <= f . y ) ::_thesis: ( f . x <= f . y implies x <= y )
proof
assume x <= y ; ::_thesis: f . x <= f . y
then compactbelow x c= compactbelow y by Th1;
then f . x c= compactbelow y by A1;
then f . x c= f . y by A1;
hence f . x <= f . y by YELLOW_1:3; ::_thesis: verum
end;
thus ( f . x <= f . y implies x <= y ) ::_thesis: verum
proof
assume f . x <= f . y ; ::_thesis: x <= y
then f . x c= f . y by YELLOW_1:3;
then f . x c= compactbelow y by A1;
then A3: compactbelow x c= compactbelow y by A1;
( ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L ) by YELLOW_0:17;
then sup (compactbelow x) <= sup (compactbelow y) by A3, YELLOW_0:34;
then sup (compactbelow x) <= y by WAYBEL_8:def_3;
hence x <= y by WAYBEL_8:def_3; ::_thesis: verum
end;
end;
now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_(InclPoset_(Ids_(CompactSublatt_L)))_holds_
ex_x9_being_set_st_
(_x9_in_the_carrier_of_L_&_y_=_f_._x9_)
let y be set ; ::_thesis: ( y in the carrier of (InclPoset (Ids (CompactSublatt L))) implies ex x9 being set st
( x9 in the carrier of L & y = f . x9 ) )
assume y in the carrier of (InclPoset (Ids (CompactSublatt L))) ; ::_thesis: ex x9 being set st
( x9 in the carrier of L & y = f . x9 )
then reconsider y9 = y as Ideal of (CompactSublatt L) by YELLOW_2:41;
reconsider y1 = y9 as non empty Subset of L by Th3;
reconsider y1 = y1 as non empty directed Subset of L by YELLOW_2:7;
set x = sup y1;
reconsider x9 = sup y1 as set ;
take x9 = x9; ::_thesis: ( x9 in the carrier of L & y = f . x9 )
thus x9 in the carrier of L ; ::_thesis: y = f . x9
A4: compactbelow (sup y1) c= y9
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in compactbelow (sup y1) or d in y9 )
assume d in compactbelow (sup y1) ; ::_thesis: d in y9
then d in { v where v is Element of L : ( sup y1 >= v & v is compact ) } by WAYBEL_8:def_2;
then consider d1 being Element of L such that
A5: d1 = d and
A6: d1 <= sup y1 and
A7: d1 is compact ;
reconsider d9 = d1 as Element of (CompactSublatt L) by A7, WAYBEL_8:def_1;
d1 << d1 by A7, WAYBEL_3:def_2;
then consider z being Element of L such that
A8: z in y1 and
A9: d1 <= z by A6, WAYBEL_3:def_1;
reconsider z9 = z as Element of (CompactSublatt L) by A8;
d9 <= z9 by A9, YELLOW_0:60;
hence d in y9 by A5, A8, WAYBEL_0:def_19; ::_thesis: verum
end;
y9 c= compactbelow (sup y1)
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in y9 or d in compactbelow (sup y1) )
assume A10: d in y9 ; ::_thesis: d in compactbelow (sup y1)
then reconsider d1 = d as Element of (CompactSublatt L) ;
reconsider d9 = d1 as Element of L by YELLOW_0:58;
y9 is_<=_than sup y1 by YELLOW_0:32;
then ( d9 is compact & d9 <= sup y1 ) by A10, LATTICE3:def_9, WAYBEL_8:def_1;
hence d in compactbelow (sup y1) by WAYBEL_8:4; ::_thesis: verum
end;
hence y = compactbelow (sup y1) by A4, XBOOLE_0:def_10
.= f . x9 by A1 ;
::_thesis: verum
end;
then A11: rng f = the carrier of (InclPoset (Ids (CompactSublatt L))) by FUNCT_2:10;
now__::_thesis:_for_x,_y_being_Element_of_L_st_f_._x_=_f_._y_holds_
x_=_y
let x, y be Element of L; ::_thesis: ( f . x = f . y implies x = y )
assume f . x = f . y ; ::_thesis: x = y
then f . x = compactbelow y by A1;
then compactbelow x = compactbelow y by A1;
then sup (compactbelow x) = y by WAYBEL_8:def_3;
hence x = y by WAYBEL_8:def_3; ::_thesis: verum
end;
then f is V13() by WAYBEL_1:def_1;
hence f is isomorphic by A11, A2, WAYBEL_0:66; ::_thesis: verum
end;
theorem :: WAYBEL13:17
for L being lower-bounded algebraic sup-Semilattice
for x being Element of L holds
( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )
proof
let L be lower-bounded algebraic sup-Semilattice; ::_thesis: for x being Element of L holds
( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )
let x be Element of L; ::_thesis: ( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )
thus ( compactbelow x is principal Ideal of (CompactSublatt L) implies x is compact ) ::_thesis: ( x is compact implies compactbelow x is principal Ideal of (CompactSublatt L) )
proof
assume compactbelow x is principal Ideal of (CompactSublatt L) ; ::_thesis: x is compact
then consider y being Element of (CompactSublatt L) such that
A1: y in compactbelow x and
A2: y is_>=_than compactbelow x by WAYBEL_0:def_21;
reconsider y9 = y as Element of L by YELLOW_0:58;
compactbelow x is Subset of (CompactSublatt L) by Th2;
then y9 is_>=_than compactbelow x by A2, YELLOW_0:62;
then y9 >= sup (compactbelow x) by YELLOW_0:32;
then A3: x <= y9 by WAYBEL_8:def_3;
( y9 <= x & y9 is compact ) by A1, WAYBEL_8:4;
hence x is compact by A3, ORDERS_2:2; ::_thesis: verum
end;
thus ( x is compact implies compactbelow x is principal Ideal of (CompactSublatt L) ) ::_thesis: verum
proof
reconsider I = compactbelow x as non empty Subset of (CompactSublatt L) by Th2;
assume A4: x is compact ; ::_thesis: compactbelow x is principal Ideal of (CompactSublatt L)
then reconsider x9 = x as Element of (CompactSublatt L) by WAYBEL_8:def_1;
compactbelow x is non empty directed Subset of L by WAYBEL_8:def_4;
then reconsider I = I as non empty directed Subset of (CompactSublatt L) by WAYBEL10:23;
now__::_thesis:_for_y,_z_being_Element_of_(CompactSublatt_L)_st_y_in_I_&_z_<=_y_holds_
z_in_I
let y, z be Element of (CompactSublatt L); ::_thesis: ( y in I & z <= y implies z in I )
reconsider y9 = y, z9 = z as Element of L by YELLOW_0:58;
assume ( y in I & z <= y ) ; ::_thesis: z in I
then ( y9 <= x & z9 <= y9 ) by WAYBEL_8:4, YELLOW_0:59;
then A5: z9 <= x by ORDERS_2:3;
z9 is compact by WAYBEL_8:def_1;
hence z in I by A5, WAYBEL_8:4; ::_thesis: verum
end;
then reconsider I = I as Ideal of (CompactSublatt L) by WAYBEL_0:def_19;
sup (compactbelow x) is_>=_than compactbelow x by YELLOW_0:32;
then x is_>=_than I by WAYBEL_8:def_3;
then A6: x9 is_>=_than I by YELLOW_0:61;
x <= x ;
then x9 in I by A4, WAYBEL_8:4;
hence compactbelow x is principal Ideal of (CompactSublatt L) by A6, WAYBEL_0:def_21; ::_thesis: verum
end;
end;
begin
theorem Th18: :: WAYBEL13:18
for L1, L2 being non empty RelStr
for X being Subset of L1
for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_<=_than X iff f . x is_<=_than f .: X )
proof
let L1, L2 be non empty RelStr ; ::_thesis: for X being Subset of L1
for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_<=_than X iff f . x is_<=_than f .: X )
let X be Subset of L1; ::_thesis: for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_<=_than X iff f . x is_<=_than f .: X )
let x be Element of L1; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
( x is_<=_than X iff f . x is_<=_than f .: X )
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies ( x is_<=_than X iff f . x is_<=_than f .: X ) )
assume A1: f is isomorphic ; ::_thesis: ( x is_<=_than X iff f . x is_<=_than f .: X )
hence ( x is_<=_than X implies f . x is_<=_than f .: X ) by YELLOW_2:13; ::_thesis: ( f . x is_<=_than f .: X implies x is_<=_than X )
thus ( f . x is_<=_than f .: X implies x is_<=_than X ) ::_thesis: verum
proof
reconsider g = f " as Function of L2,L1 by A1, WAYBEL_0:67;
assume A2: f . x is_<=_than f .: X ; ::_thesis: x is_<=_than X
g is isomorphic by A1, WAYBEL_0:68;
then A3: g . (f . x) is_<=_than g .: (f .: X) by A2, YELLOW_2:13;
A4: f " (f .: X) c= X by A1, FUNCT_1:82;
X c= the carrier of L1 ;
then X c= dom f by FUNCT_2:def_1;
then A5: X c= f " (f .: X) by FUNCT_1:76;
x in the carrier of L1 ;
then A6: x in dom f by FUNCT_2:def_1;
g .: (f .: X) = f " (f .: X) by A1, FUNCT_1:85
.= X by A4, A5, XBOOLE_0:def_10 ;
hence x is_<=_than X by A1, A6, A3, FUNCT_1:34; ::_thesis: verum
end;
end;
theorem Th19: :: WAYBEL13:19
for L1, L2 being non empty RelStr
for X being Subset of L1
for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
proof
let L1, L2 be non empty RelStr ; ::_thesis: for X being Subset of L1
for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
let X be Subset of L1; ::_thesis: for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
let x be Element of L1; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies ( x is_>=_than X iff f . x is_>=_than f .: X ) )
assume A1: f is isomorphic ; ::_thesis: ( x is_>=_than X iff f . x is_>=_than f .: X )
hence ( x is_>=_than X implies f . x is_>=_than f .: X ) by YELLOW_2:14; ::_thesis: ( f . x is_>=_than f .: X implies x is_>=_than X )
thus ( f . x is_>=_than f .: X implies x is_>=_than X ) ::_thesis: verum
proof
reconsider g = f " as Function of L2,L1 by A1, WAYBEL_0:67;
assume A2: f . x is_>=_than f .: X ; ::_thesis: x is_>=_than X
g is isomorphic by A1, WAYBEL_0:68;
then A3: g . (f . x) is_>=_than g .: (f .: X) by A2, YELLOW_2:14;
A4: f " (f .: X) c= X by A1, FUNCT_1:82;
X c= the carrier of L1 ;
then X c= dom f by FUNCT_2:def_1;
then A5: X c= f " (f .: X) by FUNCT_1:76;
x in the carrier of L1 ;
then A6: x in dom f by FUNCT_2:def_1;
g .: (f .: X) = f " (f .: X) by A1, FUNCT_1:85
.= X by A4, A5, XBOOLE_0:def_10 ;
hence x is_>=_than X by A1, A6, A3, FUNCT_1:34; ::_thesis: verum
end;
end;
theorem Th20: :: WAYBEL13:20
for L1, L2 being non empty antisymmetric RelStr
for f being Function of L1,L2 st f is isomorphic holds
( f is infs-preserving & f is sups-preserving )
proof
let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
( f is infs-preserving & f is sups-preserving )
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies ( f is infs-preserving & f is sups-preserving ) )
assume A1: f is isomorphic ; ::_thesis: ( f is infs-preserving & f is sups-preserving )
then A2: rng f = the carrier of L2 by WAYBEL_0:66;
now__::_thesis:_for_X_being_Subset_of_L1_holds_f_preserves_inf_of_X
let X be Subset of L1; ::_thesis: f preserves_inf_of X
now__::_thesis:_(_ex_inf_of_X,L1_implies_(_ex_inf_of_f_.:_X,L2_&_inf_(f_.:_X)_=_f_._(inf_X)_)_)
assume A3: ex_inf_of X,L1 ; ::_thesis: ( ex_inf_of f .: X,L2 & inf (f .: X) = f . (inf X) )
then consider a being Element of L1 such that
A4: X is_>=_than a and
A5: for b being Element of L1 st X is_>=_than b holds
a >= b by YELLOW_0:16;
A6: now__::_thesis:_for_c_being_Element_of_L2_st_f_.:_X_is_>=_than_c_holds_
f_._a_>=_c
let c be Element of L2; ::_thesis: ( f .: X is_>=_than c implies f . a >= c )
consider e being set such that
A7: e in dom f and
A8: c = f . e by A2, FUNCT_1:def_3;
reconsider e = e as Element of L1 by A7;
assume f .: X is_>=_than c ; ::_thesis: f . a >= c
then X is_>=_than e by A1, A8, Th18;
then a >= e by A5;
hence f . a >= c by A1, A8, WAYBEL_0:66; ::_thesis: verum
end;
f .: X is_>=_than f . a by A1, A4, Th18;
hence ex_inf_of f .: X,L2 by A6, YELLOW_0:16; ::_thesis: inf (f .: X) = f . (inf X)
A9: now__::_thesis:_for_b_being_Element_of_L2_st_b_is_<=_than_f_.:_X_holds_
f_._(inf_X)_>=_b
let b be Element of L2; ::_thesis: ( b is_<=_than f .: X implies f . (inf X) >= b )
consider v being set such that
A10: v in dom f and
A11: b = f . v by A2, FUNCT_1:def_3;
reconsider v = v as Element of L1 by A10;
assume b is_<=_than f .: X ; ::_thesis: f . (inf X) >= b
then v is_<=_than X by A1, A11, Th18;
then inf X >= v by A3, YELLOW_0:31;
hence f . (inf X) >= b by A1, A11, WAYBEL_0:66; ::_thesis: verum
end;
inf X is_<=_than X by A3, YELLOW_0:31;
then f . (inf X) is_<=_than f .: X by A1, Th18;
hence inf (f .: X) = f . (inf X) by A9, YELLOW_0:31; ::_thesis: verum
end;
hence f preserves_inf_of X by WAYBEL_0:def_30; ::_thesis: verum
end;
hence f is infs-preserving by WAYBEL_0:def_32; ::_thesis: f is sups-preserving
now__::_thesis:_for_X_being_Subset_of_L1_holds_f_preserves_sup_of_X
let X be Subset of L1; ::_thesis: f preserves_sup_of X
now__::_thesis:_(_ex_sup_of_X,L1_implies_(_ex_sup_of_f_.:_X,L2_&_sup_(f_.:_X)_=_f_._(sup_X)_)_)
assume A12: ex_sup_of X,L1 ; ::_thesis: ( ex_sup_of f .: X,L2 & sup (f .: X) = f . (sup X) )
then consider a being Element of L1 such that
A13: X is_<=_than a and
A14: for b being Element of L1 st X is_<=_than b holds
a <= b by YELLOW_0:15;
A15: now__::_thesis:_for_c_being_Element_of_L2_st_f_.:_X_is_<=_than_c_holds_
f_._a_<=_c
let c be Element of L2; ::_thesis: ( f .: X is_<=_than c implies f . a <= c )
consider e being set such that
A16: e in dom f and
A17: c = f . e by A2, FUNCT_1:def_3;
reconsider e = e as Element of L1 by A16;
assume f .: X is_<=_than c ; ::_thesis: f . a <= c
then X is_<=_than e by A1, A17, Th19;
then a <= e by A14;
hence f . a <= c by A1, A17, WAYBEL_0:66; ::_thesis: verum
end;
f .: X is_<=_than f . a by A1, A13, Th19;
hence ex_sup_of f .: X,L2 by A15, YELLOW_0:15; ::_thesis: sup (f .: X) = f . (sup X)
A18: now__::_thesis:_for_b_being_Element_of_L2_st_b_is_>=_than_f_.:_X_holds_
f_._(sup_X)_<=_b
let b be Element of L2; ::_thesis: ( b is_>=_than f .: X implies f . (sup X) <= b )
consider v being set such that
A19: v in dom f and
A20: b = f . v by A2, FUNCT_1:def_3;
reconsider v = v as Element of L1 by A19;
assume b is_>=_than f .: X ; ::_thesis: f . (sup X) <= b
then v is_>=_than X by A1, A20, Th19;
then sup X <= v by A12, YELLOW_0:30;
hence f . (sup X) <= b by A1, A20, WAYBEL_0:66; ::_thesis: verum
end;
sup X is_>=_than X by A12, YELLOW_0:30;
then f . (sup X) is_>=_than f .: X by A1, Th19;
hence sup (f .: X) = f . (sup X) by A18, YELLOW_0:30; ::_thesis: verum
end;
hence f preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
hence f is sups-preserving by WAYBEL_0:def_33; ::_thesis: verum
end;
registration
let L1, L2 be non empty antisymmetric RelStr ;
cluster Function-like V21( the carrier of L1, the carrier of L2) isomorphic -> infs-preserving sups-preserving for Element of K32(K33( the carrier of L1, the carrier of L2));
coherence
for b1 being Function of L1,L2 st b1 is isomorphic holds
( b1 is infs-preserving & b1 is sups-preserving ) by Th20;
end;
theorem Th21: :: WAYBEL13:21
for L1, L2, L3 being non empty transitive antisymmetric RelStr
for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is infs-preserving )
proof
let L1, L2, L3 be non empty transitive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 st f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is infs-preserving )
let f be Function of L1,L2; ::_thesis: ( f is infs-preserving & L2 is full infs-inheriting SubRelStr of L3 & L3 is complete implies ex g being Function of L1,L3 st
( f = g & g is infs-preserving ) )
assume that
A1: f is infs-preserving and
A2: L2 is full infs-inheriting SubRelStr of L3 and
A3: L3 is complete ; ::_thesis: ex g being Function of L1,L3 st
( f = g & g is infs-preserving )
the carrier of L2 c= the carrier of L3 by A2, YELLOW_0:def_13;
then reconsider g = f as Function of L1,L3 by FUNCT_2:7;
take g ; ::_thesis: ( f = g & g is infs-preserving )
thus f = g ; ::_thesis: g is infs-preserving
now__::_thesis:_for_X_being_Subset_of_L1_holds_g_preserves_inf_of_X
let X be Subset of L1; ::_thesis: g preserves_inf_of X
now__::_thesis:_(_ex_inf_of_X,L1_implies_(_ex_inf_of_g_.:_X,L3_&_inf_(g_.:_X)_=_g_._(inf_X)_)_)
A4: f preserves_inf_of X by A1, WAYBEL_0:def_32;
assume A5: ex_inf_of X,L1 ; ::_thesis: ( ex_inf_of g .: X,L3 & inf (g .: X) = g . (inf X) )
thus A6: ex_inf_of g .: X,L3 by A3, YELLOW_0:17; ::_thesis: inf (g .: X) = g . (inf X)
then "/\" ((f .: X),L3) in the carrier of L2 by A2, YELLOW_0:def_18;
hence inf (g .: X) = inf (f .: X) by A2, A6, YELLOW_0:63
.= g . (inf X) by A5, A4, WAYBEL_0:def_30 ;
::_thesis: verum
end;
hence g preserves_inf_of X by WAYBEL_0:def_30; ::_thesis: verum
end;
hence g is infs-preserving by WAYBEL_0:def_32; ::_thesis: verum
end;
theorem Th22: :: WAYBEL13:22
for L1, L2, L3 being non empty transitive antisymmetric RelStr
for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving )
proof
let L1, L2, L3 be non empty transitive antisymmetric RelStr ; ::_thesis: for f being Function of L1,L2 st f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete holds
ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving )
let f be Function of L1,L2; ::_thesis: ( f is monotone & f is directed-sups-preserving & L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving ) )
assume that
A1: ( f is monotone & f is directed-sups-preserving ) and
A2: L2 is full directed-sups-inheriting SubRelStr of L3 and
A3: L3 is complete ; ::_thesis: ex g being Function of L1,L3 st
( f = g & g is directed-sups-preserving )
the carrier of L2 c= the carrier of L3 by A2, YELLOW_0:def_13;
then reconsider g = f as Function of L1,L3 by FUNCT_2:7;
take g ; ::_thesis: ( f = g & g is directed-sups-preserving )
thus f = g ; ::_thesis: g is directed-sups-preserving
now__::_thesis:_for_X_being_Subset_of_L1_st_not_X_is_empty_&_X_is_directed_holds_
g_preserves_sup_of_X
let X be Subset of L1; ::_thesis: ( not X is empty & X is directed implies g preserves_sup_of X )
assume A4: ( not X is empty & X is directed ) ; ::_thesis: g preserves_sup_of X
then consider d being set such that
A5: d in X by XBOOLE_0:def_1;
d in the carrier of L1 by A5;
then d in dom f by FUNCT_2:def_1;
then f . d in f .: X by A5, FUNCT_1:def_6;
then A6: ( not f .: X is empty & f .: X is directed ) by A1, A4, YELLOW_2:15;
now__::_thesis:_(_ex_sup_of_X,L1_implies_(_ex_sup_of_g_.:_X,L3_&_sup_(g_.:_X)_=_g_._(sup_X)_)_)
A7: f preserves_sup_of X by A1, A4, WAYBEL_0:def_37;
assume A8: ex_sup_of X,L1 ; ::_thesis: ( ex_sup_of g .: X,L3 & sup (g .: X) = g . (sup X) )
thus ex_sup_of g .: X,L3 by A3, YELLOW_0:17; ::_thesis: sup (g .: X) = g . (sup X)
hence sup (g .: X) = sup (f .: X) by A2, A6, WAYBEL_0:7
.= g . (sup X) by A8, A7, WAYBEL_0:def_31 ;
::_thesis: verum
end;
hence g preserves_sup_of X by WAYBEL_0:def_31; ::_thesis: verum
end;
hence g is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum
end;
theorem Th23: :: WAYBEL13:23
for L being lower-bounded sup-Semilattice holds InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L)
proof
let L be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L)
CompactSublatt L is lower-bounded sup-Semilattice by Th15;
hence InclPoset (Ids (CompactSublatt L)) is CLSubFrame of BoolePoset the carrier of (CompactSublatt L) by Th8; ::_thesis: verum
end;
theorem Th24: :: WAYBEL13:24
for L being lower-bounded algebraic LATTICE ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
proof
let L be lower-bounded algebraic LATTICE; ::_thesis: ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
deffunc H1( Element of L) -> Element of K32( the carrier of L) = compactbelow $1;
A1: for y being Element of L holds H1(y) is Element of (InclPoset (Ids (CompactSublatt L)))
proof
let y be Element of L; ::_thesis: H1(y) is Element of (InclPoset (Ids (CompactSublatt L)))
reconsider comy = compactbelow y as non empty directed Subset of L by WAYBEL_8:def_4;
reconsider comy = comy as non empty Subset of (CompactSublatt L) by Th2;
reconsider comy = comy as non empty directed Subset of (CompactSublatt L) by WAYBEL10:23;
now__::_thesis:_for_x1,_z1_being_Element_of_(CompactSublatt_L)_st_x1_in_comy_&_z1_<=_x1_holds_
z1_in_comy
let x1, z1 be Element of (CompactSublatt L); ::_thesis: ( x1 in comy & z1 <= x1 implies z1 in comy )
reconsider x2 = x1, z2 = z1 as Element of L by YELLOW_0:58;
assume ( x1 in comy & z1 <= x1 ) ; ::_thesis: z1 in comy
then ( x2 <= y & z2 <= x2 ) by WAYBEL_8:4, YELLOW_0:59;
then A2: z2 <= y by ORDERS_2:3;
z2 is compact by WAYBEL_8:def_1;
hence z1 in comy by A2, WAYBEL_8:4; ::_thesis: verum
end;
then comy is lower by WAYBEL_0:def_19;
hence H1(y) is Element of (InclPoset (Ids (CompactSublatt L))) by YELLOW_2:41; ::_thesis: verum
end;
consider g1 being Function of L,(InclPoset (Ids (CompactSublatt L))) such that
A3: for y being Element of L holds g1 . y = H1(y) from FUNCT_2:sch_9(A1);
now__::_thesis:_for_k_being_set_st_k_in_the_carrier_of_(InclPoset_(Ids_(CompactSublatt_L)))_holds_
k_in_the_carrier_of_(BoolePoset_the_carrier_of_(CompactSublatt_L))
let k be set ; ::_thesis: ( k in the carrier of (InclPoset (Ids (CompactSublatt L))) implies k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) )
assume k in the carrier of (InclPoset (Ids (CompactSublatt L))) ; ::_thesis: k in the carrier of (BoolePoset the carrier of (CompactSublatt L))
then k is Ideal of (CompactSublatt L) by YELLOW_2:41;
then k is Element of (BoolePoset the carrier of (CompactSublatt L)) by WAYBEL_8:26;
hence k in the carrier of (BoolePoset the carrier of (CompactSublatt L)) ; ::_thesis: verum
end;
then the carrier of (InclPoset (Ids (CompactSublatt L))) c= the carrier of (BoolePoset the carrier of (CompactSublatt L)) by TARSKI:def_3;
then reconsider g = g1 as Function of L,(BoolePoset the carrier of (CompactSublatt L)) by FUNCT_2:7;
take g ; ::_thesis: ( g is infs-preserving & g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
A4: g1 is isomorphic by A3, Th16;
A5: InclPoset (Ids (CompactSublatt L)) is full infs-inheriting directed-sups-inheriting SubRelStr of BoolePoset the carrier of (CompactSublatt L) by Th23;
then ex g2 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g1 = g2 & g2 is infs-preserving ) by A4, Th21;
hence g is infs-preserving ; ::_thesis: ( g is directed-sups-preserving & g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
ex g3 being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g1 = g3 & g3 is directed-sups-preserving ) by A4, A5, Th22;
hence g is directed-sups-preserving ; ::_thesis: ( g is V13() & ( for x being Element of L holds g . x = compactbelow x ) )
thus g is V13() by A4; ::_thesis: for x being Element of L holds g . x = compactbelow x
let x be Element of L; ::_thesis: g . x = compactbelow x
thus g . x = compactbelow x by A3; ::_thesis: verum
end;
theorem :: WAYBEL13:25
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 lower-bounded algebraic LATTICE ) holds
product J is lower-bounded algebraic LATTICE
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 lower-bounded algebraic LATTICE ) holds
product J is lower-bounded algebraic LATTICE
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is lower-bounded algebraic LATTICE ) implies product J is lower-bounded algebraic LATTICE )
assume A1: for i being Element of I holds J . i is lower-bounded algebraic LATTICE ; ::_thesis: product J is lower-bounded algebraic LATTICE
then A2: for i being Element of I holds J . i is complete LATTICE ;
then reconsider L = product J as non empty lower-bounded LATTICE by WAYBEL_3:31;
for i being Element of I holds J . i is antisymmetric by A1;
then A3: product J is antisymmetric by WAYBEL_3:30;
now__::_thesis:_for_x_being_Element_of_(product_J)_holds_x_=_sup_(compactbelow_x)
let x be Element of (product J); ::_thesis: x = sup (compactbelow x)
A4: for i being Element of I holds sup (compactbelow (x . i)) = (sup (compactbelow x)) . i
proof
let i be Element of I; ::_thesis: sup (compactbelow (x . i)) = (sup (compactbelow x)) . i
A5: compactbelow (x . i) c= pi ((compactbelow x),i)
proof
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
defpred S1[ set ] means $1 = i;
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in compactbelow (x . i) or v in pi ((compactbelow x),i) )
assume v in compactbelow (x . i) ; ::_thesis: v in pi ((compactbelow x),i)
then v in { y where y is Element of (J . i) : ( x . i >= y & y is compact ) } by WAYBEL_8:def_2;
then consider v1 being Element of (J . i) such that
A6: v1 = v and
A7: x . i >= v1 and
A8: v1 is compact ;
deffunc H2( set ) -> Element of (J . i) = v1;
consider f being Function such that
A9: dom f = I and
A10: for j being Element of I holds
( ( S1[j] implies f . j = H2(j) ) & ( not S1[j] implies f . j = H1(j) ) ) from PARTFUN1:sch_4();
A11: f . i = v1 by A10;
now__::_thesis:_for_k_being_Element_of_I_holds_f_._k_is_Element_of_(J_._k)
let k be Element of I; ::_thesis: f . k is Element of (J . k)
now__::_thesis:_f_._k_is_Element_of_(J_._k)
percases ( k = i or k <> i ) ;
suppose k = i ; ::_thesis: f . k is Element of (J . k)
hence f . k is Element of (J . k) by A10; ::_thesis: verum
end;
suppose k <> i ; ::_thesis: f . k is Element of (J . k)
then f . k = Bottom (J . k) by A10;
hence f . k is Element of (J . k) ; ::_thesis: verum
end;
end;
end;
hence f . k is Element of (J . k) ; ::_thesis: verum
end;
then reconsider f = f as Element of (product J) by A9, WAYBEL_3:27;
now__::_thesis:_for_k_being_Element_of_I_holds_f_._k_<=_x_._k
let k be Element of I; ::_thesis: f . k <= x . k
A12: J . k is lower-bounded algebraic LATTICE by A1;
now__::_thesis:_f_._k_<=_x_._k
percases ( k = i or k <> i ) ;
suppose k = i ; ::_thesis: f . k <= x . k
hence f . k <= x . k by A7, A10; ::_thesis: verum
end;
suppose k <> i ; ::_thesis: f . k <= x . k
then f . k = Bottom (J . k) by A10;
hence f . k <= x . k by A12, YELLOW_0:44; ::_thesis: verum
end;
end;
end;
hence f . k <= x . k ; ::_thesis: verum
end;
then A13: f <= x by WAYBEL_3:28;
A14: now__::_thesis:_for_k_being_Element_of_I_holds_f_._k_<<_f_._k
let k be Element of I; ::_thesis: f . k << f . k
A15: J . k is lower-bounded algebraic LATTICE by A1;
now__::_thesis:_f_._k_<<_f_._k
percases ( k = i or k <> i ) ;
supposeA16: k = i ; ::_thesis: f . k << f . k
then f . k = v1 by A10;
hence f . k << f . k by A8, A16, WAYBEL_3:def_2; ::_thesis: verum
end;
suppose k <> i ; ::_thesis: f . k << f . k
then f . k = Bottom (J . k) by A10;
then f . k is compact by A15, WAYBEL_3:15;
hence f . k << f . k by WAYBEL_3:def_2; ::_thesis: verum
end;
end;
end;
hence f . k << f . k ; ::_thesis: verum
end;
ex K being finite Subset of I st
for k being Element of I st not k in K holds
f . k = Bottom (J . k)
proof
take K = {i}; ::_thesis: for k being Element of I st not k in K holds
f . k = Bottom (J . k)
let k be Element of I; ::_thesis: ( not k in K implies f . k = Bottom (J . k) )
assume not k in K ; ::_thesis: f . k = Bottom (J . k)
then k <> i by TARSKI:def_1;
hence f . k = Bottom (J . k) by A10; ::_thesis: verum
end;
then f << f by A2, A14, WAYBEL_3:33;
then f is compact by WAYBEL_3:def_2;
then f in compactbelow x by A13, WAYBEL_8:4;
hence v in pi ((compactbelow x),i) by A6, A11, CARD_3:def_6; ::_thesis: verum
end;
pi ((compactbelow x),i) c= compactbelow (x . i)
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in pi ((compactbelow x),i) or v in compactbelow (x . i) )
assume v in pi ((compactbelow x),i) ; ::_thesis: v in compactbelow (x . i)
then consider f being Function such that
A17: f in compactbelow x and
A18: v = f . i by CARD_3:def_6;
f in { y where y is Element of (product J) : ( x >= y & y is compact ) } by A17, WAYBEL_8:def_2;
then consider f1 being Element of (product J) such that
A19: f1 = f and
A20: x >= f1 and
A21: f1 is compact ;
f1 << f1 by A21, WAYBEL_3:def_2;
then f1 . i << f1 . i by A2, WAYBEL_3:33;
then A22: f1 . i is compact by WAYBEL_3:def_2;
f1 . i <= x . i by A20, WAYBEL_3:28;
hence v in compactbelow (x . i) by A18, A19, A22, WAYBEL_8:4; ::_thesis: verum
end;
hence sup (compactbelow (x . i)) = sup (pi ((compactbelow x),i)) by A5, XBOOLE_0:def_10
.= (sup (compactbelow x)) . i by A2, WAYBEL_3:32 ;
::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_I_holds_(sup_(compactbelow_x))_._i_<=_x_._i
let i be Element of I; ::_thesis: (sup (compactbelow x)) . i <= x . i
J . i is satisfying_axiom_K by A1;
then x . i = sup (compactbelow (x . i)) by WAYBEL_8:def_3;
hence (sup (compactbelow x)) . i <= x . i by A4; ::_thesis: verum
end;
then A23: sup (compactbelow x) <= x by WAYBEL_3:28;
now__::_thesis:_for_i_being_Element_of_I_holds_x_._i_<=_(sup_(compactbelow_x))_._i
let i be Element of I; ::_thesis: x . i <= (sup (compactbelow x)) . i
J . i is satisfying_axiom_K by A1;
then x . i = sup (compactbelow (x . i)) by WAYBEL_8:def_3;
hence x . i <= (sup (compactbelow x)) . i by A4; ::_thesis: verum
end;
then x <= sup (compactbelow x) by WAYBEL_3:28;
hence x = sup (compactbelow x) by A3, A23, YELLOW_0:def_3; ::_thesis: verum
end;
then A24: product J is satisfying_axiom_K by WAYBEL_8:def_3;
A25: for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed )
proof
let x be Element of L; ::_thesis: ( not compactbelow x is empty & compactbelow x is directed )
now__::_thesis:_for_c,_d_being_Element_of_L_st_c_in_compactbelow_x_&_d_in_compactbelow_x_holds_
ex_e_being_Element_of_the_carrier_of_L_st_
(_e_in_compactbelow_x_&_c_<=_e_&_d_<=_e_)
let c, d be Element of L; ::_thesis: ( c in compactbelow x & d in compactbelow x implies ex e being Element of the carrier of L st
( e in compactbelow x & c <= e & d <= e ) )
assume that
A26: c in compactbelow x and
A27: d in compactbelow x ; ::_thesis: ex e being Element of the carrier of L st
( e in compactbelow x & c <= e & d <= e )
d is compact by A27, WAYBEL_8:4;
then ( d <= c "\/" d & d << d ) by WAYBEL_3:def_2, YELLOW_0:22;
then A28: d << c "\/" d by WAYBEL_3:2;
c is compact by A26, WAYBEL_8:4;
then ( c <= c "\/" d & c << c ) by WAYBEL_3:def_2, YELLOW_0:22;
then c << c "\/" d by WAYBEL_3:2;
then c "\/" d << c "\/" d by A28, WAYBEL_3:3;
then A29: c "\/" d is compact by WAYBEL_3:def_2;
take e = c "\/" d; ::_thesis: ( e in compactbelow x & c <= e & d <= e )
( c <= x & d <= x ) by A26, A27, WAYBEL_8:4;
then c "\/" d <= x by YELLOW_0:22;
hence e in compactbelow x by A29, WAYBEL_8:4; ::_thesis: ( c <= e & d <= e )
thus ( c <= e & d <= e ) by YELLOW_0:22; ::_thesis: verum
end;
hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:def_1; ::_thesis: verum
end;
L is up-complete by A2, WAYBEL_3:31;
hence product J is lower-bounded algebraic LATTICE by A25, A24, WAYBEL_8:def_4; ::_thesis: verum
end;
Lm1: for L being lower-bounded LATTICE st L is algebraic holds
ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
proof
let L be lower-bounded LATTICE; ::_thesis: ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) )
assume A1: L is algebraic ; ::_thesis: ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
then reconsider L9 = L as lower-bounded algebraic LATTICE ;
take X = the carrier of (CompactSublatt L); ::_thesis: ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
consider g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) such that
A2: g is infs-preserving and
A3: g is directed-sups-preserving and
A4: g is V13() and
A5: for x being Element of L holds g . x = compactbelow x by A1, Th24;
reconsider S = Image g as non empty full SubRelStr of BoolePoset X ;
take S ; ::_thesis: ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
A6: L9 is complete ;
hence S is infs-inheriting by A2, YELLOW_2:33; ::_thesis: ( S is directed-sups-inheriting & L,S are_isomorphic )
A7: rng g = the carrier of S by YELLOW_0:def_15;
dom g = the carrier of L by FUNCT_2:def_1;
then reconsider g1 = g as Function of L,S by A7, FUNCT_2:1;
now__::_thesis:_for_x,_y_being_Element_of_L_holds_
(_(_x_<=_y_implies_g1_._x_<=_g1_._y_)_&_(_g1_._x_<=_g1_._y_implies_x_<=_y_)_)
let x, y be Element of L; ::_thesis: ( ( x <= y implies g1 . x <= g1 . y ) & ( g1 . x <= g1 . y implies x <= y ) )
thus ( x <= y implies g1 . x <= g1 . y ) ::_thesis: ( g1 . x <= g1 . y implies x <= y )
proof
assume x <= y ; ::_thesis: g1 . x <= g1 . y
then compactbelow x c= compactbelow y by Th1;
then g . x c= compactbelow y by A5;
then g . x c= g . y by A5;
then g . x <= g . y by YELLOW_1:2;
hence g1 . x <= g1 . y by YELLOW_0:60; ::_thesis: verum
end;
thus ( g1 . x <= g1 . y implies x <= y ) ::_thesis: verum
proof
assume g1 . x <= g1 . y ; ::_thesis: x <= y
then g . x <= g . y by YELLOW_0:59;
then g . x c= g . y by YELLOW_1:2;
then g . x c= compactbelow y by A5;
then A8: compactbelow x c= compactbelow y by A5;
( ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L ) by A6, YELLOW_0:17;
then sup (compactbelow x) <= sup (compactbelow y) by A8, YELLOW_0:34;
then x <= sup (compactbelow y) by A1, WAYBEL_8:def_3;
hence x <= y by A1, WAYBEL_8:def_3; ::_thesis: verum
end;
end;
then A9: g1 is isomorphic by A4, A7, WAYBEL_0:66;
then reconsider f1 = g1 " as Function of S,L by WAYBEL_0:67;
A10: f1 is isomorphic by A9, WAYBEL_0:68;
now__::_thesis:_for_Y_being_directed_Subset_of_S_st_Y_<>_{}_&_ex_sup_of_Y,_BoolePoset_X_holds_
"\/"_(Y,(BoolePoset_X))_in_the_carrier_of_S
let Y be directed Subset of S; ::_thesis: ( Y <> {} & ex_sup_of Y, BoolePoset X implies "\/" (Y,(BoolePoset X)) in the carrier of S )
assume that
A11: Y <> {} and
ex_sup_of Y, BoolePoset X ; ::_thesis: "\/" (Y,(BoolePoset X)) in the carrier of S
now__::_thesis:_for_X2_being_finite_Subset_of_(f1_.:_Y)_ex_f1y1_being_Element_of_the_carrier_of_L_st_
(_f1y1_in_f1_.:_Y_&_f1y1_is_>=_than_X2_)
let X2 be finite Subset of (f1 .: Y); ::_thesis: ex f1y1 being Element of the carrier of L st
( f1y1 in f1 .: Y & f1y1 is_>=_than X2 )
A12: g1 " (g1 .: X2) c= X2 by A4, FUNCT_1:82;
now__::_thesis:_for_v_being_set_st_v_in_g1_.:_X2_holds_
v_in_Y
let v be set ; ::_thesis: ( v in g1 .: X2 implies v in Y )
assume v in g1 .: X2 ; ::_thesis: v in Y
then ex u being set st
( u in dom g1 & u in X2 & v = g1 . u ) by FUNCT_1:def_6;
then v in g1 .: (f1 .: Y) by FUNCT_1:def_6;
then v in g1 .: (g1 " Y) by A4, FUNCT_1:85;
hence v in Y by A7, FUNCT_1:77; ::_thesis: verum
end;
then reconsider Y1 = g1 .: X2 as finite Subset of Y by TARSKI:def_3;
consider y1 being Element of S such that
A13: y1 in Y and
A14: y1 is_>=_than Y1 by A11, WAYBEL_0:1;
take f1y1 = f1 . y1; ::_thesis: ( f1y1 in f1 .: Y & f1y1 is_>=_than X2 )
y1 in the carrier of S ;
then y1 in dom f1 by FUNCT_2:def_1;
hence f1y1 in f1 .: Y by A13, FUNCT_1:def_6; ::_thesis: f1y1 is_>=_than X2
X2 c= the carrier of L by XBOOLE_1:1;
then X2 c= dom g1 by FUNCT_2:def_1;
then A15: X2 c= g1 " (g1 .: X2) by FUNCT_1:76;
f1 .: Y1 = g1 " (g1 .: X2) by A4, FUNCT_1:85
.= X2 by A15, A12, XBOOLE_0:def_10 ;
hence f1y1 is_>=_than X2 by A10, A14, Th19; ::_thesis: verum
end;
then reconsider X1 = f1 .: Y as non empty directed Subset of L by WAYBEL_0:1;
sup X1 in the carrier of L ;
then sup X1 in dom g by FUNCT_2:def_1;
then A16: g . (sup X1) in rng g by FUNCT_1:def_3;
( ex_sup_of X1,L & g preserves_sup_of X1 ) by A6, A3, WAYBEL_0:def_37, YELLOW_0:17;
then A17: sup (g .: X1) in rng g by A16, WAYBEL_0:def_31;
g .: X1 = g .: (g1 " Y) by A4, FUNCT_1:85
.= Y by A7, FUNCT_1:77 ;
hence "\/" (Y,(BoolePoset X)) in the carrier of S by A17, YELLOW_0:def_15; ::_thesis: verum
end;
hence S is directed-sups-inheriting by WAYBEL_0:def_4; ::_thesis: L,S are_isomorphic
thus L,S are_isomorphic by A9, WAYBEL_1:def_8; ::_thesis: verum
end;
theorem Th26: :: WAYBEL13:26
for L1, L2 being non empty RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
L1,L2 are_isomorphic
proof
let L1, L2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies L1,L2 are_isomorphic )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: L1,L2 are_isomorphic
ex f being Function of L1,L2 st f is isomorphic
proof
reconsider f = id the carrier of L1 as Function of L1,L2 by A1;
take f ; ::_thesis: f is isomorphic
now__::_thesis:_for_z_being_set_st_z_in_the_carrier_of_L2_holds_
ex_v_being_set_st_
(_v_in_the_carrier_of_L1_&_z_=_f_._v_)
let z be set ; ::_thesis: ( z in the carrier of L2 implies ex v being set st
( v in the carrier of L1 & z = f . v ) )
assume A2: z in the carrier of L2 ; ::_thesis: ex v being set st
( v in the carrier of L1 & z = f . v )
take v = z; ::_thesis: ( v in the carrier of L1 & z = f . v )
thus v in the carrier of L1 by A1, A2; ::_thesis: z = f . v
thus z = f . v by A1, A2, FUNCT_1:18; ::_thesis: verum
end;
then A3: rng f = the carrier of L2 by FUNCT_2:10;
for x, y being Element of L1 holds
( x <= y iff f . x <= f . y )
proof
let x, y be Element of L1; ::_thesis: ( x <= y iff f . x <= f . y )
A4: ( f . x = x & f . y = y ) by FUNCT_1:18;
hence ( x <= y implies f . x <= f . y ) by A1, YELLOW_0:1; ::_thesis: ( f . x <= f . y implies x <= y )
thus ( f . x <= f . y implies x <= y ) by A1, A4, YELLOW_0:1; ::_thesis: verum
end;
hence f is isomorphic by A3, WAYBEL_0:66; ::_thesis: verum
end;
hence L1,L2 are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum
end;
Lm2: for L being LATTICE st ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
proof
let L be LATTICE; ::_thesis: ( ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) )
given X being non empty set , S being full SubRelStr of BoolePoset X such that A1: S is infs-inheriting and
A2: S is directed-sups-inheriting and
A3: L,S are_isomorphic ; ::_thesis: ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
reconsider S9 = S as closure System of BoolePoset X by A1;
take X ; ::_thesis: ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
reconsider c = closure_op S9 as closure Function of (BoolePoset X),(BoolePoset X) ;
take c ; ::_thesis: ( c is directed-sups-preserving & L, Image c are_isomorphic )
thus c is directed-sups-preserving by A2; ::_thesis: L, Image c are_isomorphic
Image c = RelStr(# the carrier of S, the InternalRel of S #) by WAYBEL10:18;
then S, Image c are_isomorphic by Th26;
hence L, Image c are_isomorphic by A3, WAYBEL_1:7; ::_thesis: verum
end;
Lm3: for L being LATTICE st ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) holds
ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
proof
let L be LATTICE; ::_thesis: ( ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) )
given X being set , S being full SubRelStr of BoolePoset X such that A1: S is infs-inheriting and
A2: S is directed-sups-inheriting and
A3: L,S are_isomorphic ; ::_thesis: ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
reconsider S9 = S as closure System of BoolePoset X by A1;
take X ; ::_thesis: ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
reconsider c = closure_op S9 as closure Function of (BoolePoset X),(BoolePoset X) ;
take c ; ::_thesis: ( c is directed-sups-preserving & L, Image c are_isomorphic )
thus c is directed-sups-preserving by A2; ::_thesis: L, Image c are_isomorphic
Image c = RelStr(# the carrier of S, the InternalRel of S #) by WAYBEL10:18;
then S, Image c are_isomorphic by Th26;
hence L, Image c are_isomorphic by A3, WAYBEL_1:7; ::_thesis: verum
end;
Lm4: for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 st x << y holds
f . x << f . y
proof
let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 st x << y holds
f . x << f . y
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x, y being Element of L1 st x << y holds
f . x << f . y )
assume A1: f is isomorphic ; ::_thesis: for x, y being Element of L1 st x << y holds
f . x << f . y
then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67;
let x, y be Element of L1; ::_thesis: ( x << y implies f . x << f . y )
A2: g is isomorphic by A1, WAYBEL_0:68;
assume A3: x << y ; ::_thesis: f . x << f . y
now__::_thesis:_for_X_being_non_empty_directed_Subset_of_L2_st_f_._y_<=_sup_X_holds_
ex_fc_being_Element_of_the_carrier_of_L2_st_
(_fc_in_X_&_f_._x_<=_fc_)
let X be non empty directed Subset of L2; ::_thesis: ( f . y <= sup X implies ex fc being Element of the carrier of L2 st
( fc in X & f . x <= fc ) )
y in the carrier of L1 ;
then A4: y in dom f by FUNCT_2:def_1;
X c= the carrier of L2 ;
then A5: X c= rng f by A1, WAYBEL_0:66;
now__::_thesis:_for_Y1_being_finite_Subset_of_(g_.:_X)_ex_gy1_being_Element_of_the_carrier_of_L1_st_
(_gy1_in_g_.:_X_&_gy1_is_>=_than_Y1_)
let Y1 be finite Subset of (g .: X); ::_thesis: ex gy1 being Element of the carrier of L1 st
( gy1 in g .: X & gy1 is_>=_than Y1 )
A6: f " (f .: Y1) c= Y1 by A1, FUNCT_1:82;
now__::_thesis:_for_v_being_set_st_v_in_f_.:_Y1_holds_
v_in_X
let v be set ; ::_thesis: ( v in f .: Y1 implies v in X )
assume v in f .: Y1 ; ::_thesis: v in X
then ex u being set st
( u in dom f & u in Y1 & v = f . u ) by FUNCT_1:def_6;
then v in f .: (g .: X) by FUNCT_1:def_6;
then v in f .: (f " X) by A1, FUNCT_1:85;
hence v in X by A5, FUNCT_1:77; ::_thesis: verum
end;
then reconsider X1 = f .: Y1 as finite Subset of X by TARSKI:def_3;
consider y1 being Element of L2 such that
A7: y1 in X and
A8: y1 is_>=_than X1 by WAYBEL_0:1;
take gy1 = g . y1; ::_thesis: ( gy1 in g .: X & gy1 is_>=_than Y1 )
y1 in the carrier of L2 ;
then y1 in dom g by FUNCT_2:def_1;
hence gy1 in g .: X by A7, FUNCT_1:def_6; ::_thesis: gy1 is_>=_than Y1
Y1 c= the carrier of L1 by XBOOLE_1:1;
then Y1 c= dom f by FUNCT_2:def_1;
then A9: Y1 c= f " (f .: Y1) by FUNCT_1:76;
g .: X1 = f " (f .: Y1) by A1, FUNCT_1:85
.= Y1 by A9, A6, XBOOLE_0:def_10 ;
hence gy1 is_>=_than Y1 by A2, A8, Th19; ::_thesis: verum
end;
then reconsider Y = g .: X as non empty directed Subset of L1 by WAYBEL_0:1;
A10: ( ex_sup_of X,L2 & g preserves_sup_of X ) by A2, WAYBEL_0:75, WAYBEL_0:def_33;
assume f . y <= sup X ; ::_thesis: ex fc being Element of the carrier of L2 st
( fc in X & f . x <= fc )
then g . (f . y) <= g . (sup X) by A2, WAYBEL_0:66;
then y <= g . (sup X) by A1, A4, FUNCT_1:34;
then y <= sup Y by A10, WAYBEL_0:def_31;
then consider c being Element of L1 such that
A11: c in Y and
A12: x <= c by A3, WAYBEL_3:def_1;
take fc = f . c; ::_thesis: ( fc in X & f . x <= fc )
c in the carrier of L1 ;
then c in dom f by FUNCT_2:def_1;
then f . c in f .: Y by A11, FUNCT_1:def_6;
then f . c in f .: (f " X) by A1, FUNCT_1:85;
hence fc in X by A5, FUNCT_1:77; ::_thesis: f . x <= fc
thus f . x <= fc by A1, A12, WAYBEL_0:66; ::_thesis: verum
end;
hence f . x << f . y by WAYBEL_3:def_1; ::_thesis: verum
end;
theorem Th27: :: WAYBEL13:27
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 holds
( x << y iff f . x << f . y )
proof
let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 holds
( x << y iff f . x << f . y )
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x, y being Element of L1 holds
( x << y iff f . x << f . y ) )
assume A1: f is isomorphic ; ::_thesis: for x, y being Element of L1 holds
( x << y iff f . x << f . y )
then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67;
let x, y be Element of L1; ::_thesis: ( x << y iff f . x << f . y )
thus ( x << y implies f . x << f . y ) by A1, Lm4; ::_thesis: ( f . x << f . y implies x << y )
thus ( f . x << f . y implies x << y ) ::_thesis: verum
proof
y in the carrier of L1 ;
then A2: y in dom f by FUNCT_2:def_1;
x in the carrier of L1 ;
then A3: x in dom f by FUNCT_2:def_1;
assume f . x << f . y ; ::_thesis: x << y
then g . (f . x) << g . (f . y) by A1, Lm4, WAYBEL_0:68;
then x << g . (f . y) by A1, A3, FUNCT_1:34;
hence x << y by A1, A2, FUNCT_1:34; ::_thesis: verum
end;
end;
theorem Th28: :: WAYBEL13:28
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds
( x is compact iff f . x is compact )
proof
let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds
( x is compact iff f . x is compact )
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x being Element of L1 holds
( x is compact iff f . x is compact ) )
assume A1: f is isomorphic ; ::_thesis: for x being Element of L1 holds
( x is compact iff f . x is compact )
let x be Element of L1; ::_thesis: ( x is compact iff f . x is compact )
thus ( x is compact implies f . x is compact ) ::_thesis: ( f . x is compact implies x is compact )
proof
assume x is compact ; ::_thesis: f . x is compact
then x << x by WAYBEL_3:def_2;
then f . x << f . x by A1, Th27;
hence f . x is compact by WAYBEL_3:def_2; ::_thesis: verum
end;
thus ( f . x is compact implies x is compact ) ::_thesis: verum
proof
assume f . x is compact ; ::_thesis: x is compact
then f . x << f . x by WAYBEL_3:def_2;
then x << x by A1, Th27;
hence x is compact by WAYBEL_3:def_2; ::_thesis: verum
end;
end;
theorem Th29: :: WAYBEL13:29
for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)
proof
let L1, L2 be non empty up-complete Poset; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)
let f be Function of L1,L2; ::_thesis: ( f is isomorphic implies for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x) )
assume A1: f is isomorphic ; ::_thesis: for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)
then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67;
let x be Element of L1; ::_thesis: f .: (compactbelow x) = compactbelow (f . x)
A2: g is isomorphic by A1, WAYBEL_0:68;
A3: compactbelow (f . x) c= f .: (compactbelow x)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in compactbelow (f . x) or z in f .: (compactbelow x) )
x in the carrier of L1 ;
then A4: x in dom f by FUNCT_2:def_1;
assume z in compactbelow (f . x) ; ::_thesis: z in f .: (compactbelow x)
then z in { y where y is Element of L2 : ( f . x >= y & y is compact ) } by WAYBEL_8:def_2;
then consider z1 being Element of L2 such that
A5: z1 = z and
A6: f . x >= z1 and
A7: z1 is compact ;
A8: g . z1 is compact by A2, A7, Th28;
g . z1 <= g . (f . x) by A2, A6, WAYBEL_0:66;
then g . z1 <= x by A1, A4, FUNCT_1:34;
then A9: g . z1 in compactbelow x by A8, WAYBEL_8:4;
z1 in the carrier of L2 ;
then A10: z1 in rng f by A1, WAYBEL_0:66;
g . z1 in the carrier of L1 ;
then g . z1 in dom f by FUNCT_2:def_1;
then f . (g . z1) in f .: (compactbelow x) by A9, FUNCT_1:def_6;
hence z in f .: (compactbelow x) by A1, A5, A10, FUNCT_1:35; ::_thesis: verum
end;
f .: (compactbelow x) c= compactbelow (f . x)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in f .: (compactbelow x) or z in compactbelow (f . x) )
assume z in f .: (compactbelow x) ; ::_thesis: z in compactbelow (f . x)
then consider u being set such that
u in dom f and
A11: u in compactbelow x and
A12: z = f . u by FUNCT_1:def_6;
u in { y where y is Element of L1 : ( x >= y & y is compact ) } by A11, WAYBEL_8:def_2;
then consider u1 being Element of L1 such that
A13: u1 = u and
A14: ( x >= u1 & u1 is compact ) ;
( f . u1 <= f . x & f . u1 is compact ) by A1, A14, Th28, WAYBEL_0:66;
hence z in compactbelow (f . x) by A12, A13, WAYBEL_8:4; ::_thesis: verum
end;
hence f .: (compactbelow x) = compactbelow (f . x) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th30: :: WAYBEL13:30
for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is up-complete holds
L2 is up-complete
proof
let L1, L2 be non empty Poset; ::_thesis: ( L1,L2 are_isomorphic & L1 is up-complete implies L2 is up-complete )
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is up-complete ; ::_thesis: L2 is up-complete
consider f being Function of L1,L2 such that
A3: f is isomorphic by A1, WAYBEL_1:def_8;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
A4: g is isomorphic by A3, WAYBEL_0:68;
now__::_thesis:_for_Y_being_non_empty_directed_Subset_of_L2_holds_ex_sup_of_Y,L2
let Y be non empty directed Subset of L2; ::_thesis: ex_sup_of Y,L2
Y c= the carrier of L2 ;
then A5: Y c= rng f by A3, WAYBEL_0:66;
now__::_thesis:_for_X1_being_finite_Subset_of_(g_.:_Y)_ex_gy1_being_Element_of_the_carrier_of_L1_st_
(_gy1_in_g_.:_Y_&_gy1_is_>=_than_X1_)
let X1 be finite Subset of (g .: Y); ::_thesis: ex gy1 being Element of the carrier of L1 st
( gy1 in g .: Y & gy1 is_>=_than X1 )
A6: f " (f .: X1) c= X1 by A3, FUNCT_1:82;
now__::_thesis:_for_v_being_set_st_v_in_f_.:_X1_holds_
v_in_Y
let v be set ; ::_thesis: ( v in f .: X1 implies v in Y )
assume v in f .: X1 ; ::_thesis: v in Y
then ex u being set st
( u in dom f & u in X1 & v = f . u ) by FUNCT_1:def_6;
then v in f .: (g .: Y) by FUNCT_1:def_6;
then v in f .: (f " Y) by A3, FUNCT_1:85;
hence v in Y by A5, FUNCT_1:77; ::_thesis: verum
end;
then reconsider Y1 = f .: X1 as finite Subset of Y by TARSKI:def_3;
consider y1 being Element of L2 such that
A7: y1 in Y and
A8: y1 is_>=_than Y1 by WAYBEL_0:1;
take gy1 = g . y1; ::_thesis: ( gy1 in g .: Y & gy1 is_>=_than X1 )
y1 in the carrier of L2 ;
then y1 in dom g by FUNCT_2:def_1;
hence gy1 in g .: Y by A7, FUNCT_1:def_6; ::_thesis: gy1 is_>=_than X1
X1 c= the carrier of L1 by XBOOLE_1:1;
then X1 c= dom f by FUNCT_2:def_1;
then A9: X1 c= f " (f .: X1) by FUNCT_1:76;
g .: Y1 = f " (f .: X1) by A3, FUNCT_1:85
.= X1 by A9, A6, XBOOLE_0:def_10 ;
hence gy1 is_>=_than X1 by A4, A8, Th19; ::_thesis: verum
end;
then reconsider X = g .: Y as non empty directed Subset of L1 by WAYBEL_0:1;
ex_sup_of X,L1 by A2, WAYBEL_0:75;
then consider x being Element of L1 such that
A10: X is_<=_than x and
A11: for b being Element of L1 st X is_<=_than b holds
x <= b by YELLOW_0:15;
A12: now__::_thesis:_for_y_being_Element_of_L2_st_Y_is_<=_than_y_holds_
f_._x_<=_y
let y be Element of L2; ::_thesis: ( Y is_<=_than y implies f . x <= y )
assume Y is_<=_than y ; ::_thesis: f . x <= y
then X is_<=_than g . y by A4, Th19;
then x <= g . y by A11;
then A13: f . x <= f . (g . y) by A3, WAYBEL_0:66;
y in the carrier of L2 ;
then y in dom g by FUNCT_2:def_1;
then y in rng f by A3, FUNCT_1:33;
hence f . x <= y by A3, A13, FUNCT_1:35; ::_thesis: verum
end;
f .: X = f .: (f " Y) by A3, FUNCT_1:85
.= Y by A5, FUNCT_1:77 ;
then Y is_<=_than f . x by A3, A10, Th19;
hence ex_sup_of Y,L2 by A12, YELLOW_0:15; ::_thesis: verum
end;
hence L2 is up-complete by WAYBEL_0:75; ::_thesis: verum
end;
theorem Th31: :: WAYBEL13:31
for L1, L2 being non empty Poset st L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K holds
L2 is satisfying_axiom_K
proof
let L1, L2 be non empty Poset; ::_thesis: ( L1,L2 are_isomorphic & L1 is complete & L1 is satisfying_axiom_K implies L2 is satisfying_axiom_K )
assume that
A1: L1,L2 are_isomorphic and
A2: ( L1 is complete & L1 is satisfying_axiom_K ) ; ::_thesis: L2 is satisfying_axiom_K
consider f being Function of L1,L2 such that
A3: f is isomorphic by A1, WAYBEL_1:def_8;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
now__::_thesis:_for_x_being_Element_of_L2_holds_x_=_sup_(compactbelow_x)
let x be Element of L2; ::_thesis: x = sup (compactbelow x)
A4: ( f preserves_sup_of compactbelow (g . x) & ex_sup_of compactbelow (g . x),L1 ) by A2, A3, WAYBEL_0:def_33, YELLOW_0:17;
A5: L2 is non empty up-complete Poset by A1, A2, Th30;
x in the carrier of L2 ;
then x in dom g by FUNCT_2:def_1;
then A6: x in rng f by A3, FUNCT_1:33;
hence x = f . (g . x) by A3, FUNCT_1:35
.= f . (sup (compactbelow (g . x))) by A2, WAYBEL_8:def_3
.= sup (f .: (compactbelow (g . x))) by A4, WAYBEL_0:def_31
.= sup (compactbelow (f . (g . x))) by A2, A3, A5, Th29
.= sup (compactbelow x) by A3, A6, FUNCT_1:35 ;
::_thesis: verum
end;
hence L2 is satisfying_axiom_K by WAYBEL_8:def_3; ::_thesis: verum
end;
theorem Th32: :: WAYBEL13:32
for L1, L2 being sup-Semilattice st L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic holds
L2 is algebraic
proof
let L1, L2 be sup-Semilattice; ::_thesis: ( L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic implies L2 is algebraic )
assume that
A1: L1,L2 are_isomorphic and
A2: ( L1 is lower-bounded & L1 is algebraic ) ; ::_thesis: L2 is algebraic
consider f being Function of L1,L2 such that
A3: f is isomorphic by A1, WAYBEL_1:def_8;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
A4: g is isomorphic by A3, WAYBEL_0:68;
A5: now__::_thesis:_for_y_being_Element_of_L2_holds_
(_not_compactbelow_y_is_empty_&_compactbelow_y_is_directed_)
let y be Element of L2; ::_thesis: ( not compactbelow y is empty & compactbelow y is directed )
y in the carrier of L2 ;
then y in dom g by FUNCT_2:def_1;
then A6: y in rng f by A3, FUNCT_1:33;
A7: L2 is non empty up-complete Poset by A1, A2, Th30;
A8: ( not compactbelow (g . y) is empty & compactbelow (g . y) is directed ) by A2, WAYBEL_8:def_4;
now__::_thesis:_for_Y_being_finite_Subset_of_(compactbelow_(f_._(g_._y)))_ex_fx_being_Element_of_the_carrier_of_L2_st_
(_fx_in_compactbelow_(f_._(g_._y))_&_fx_is_>=_than_Y_)
let Y be finite Subset of (compactbelow (f . (g . y))); ::_thesis: ex fx being Element of the carrier of L2 st
( fx in compactbelow (f . (g . y)) & fx is_>=_than Y )
Y c= the carrier of L2 by XBOOLE_1:1;
then A9: Y c= rng f by A3, WAYBEL_0:66;
now__::_thesis:_for_z_being_set_st_z_in_g_.:_Y_holds_
z_in_compactbelow_(g_._y)
let z be set ; ::_thesis: ( z in g .: Y implies z in compactbelow (g . y) )
assume z in g .: Y ; ::_thesis: z in compactbelow (g . y)
then consider v being set such that
A10: v in dom g and
A11: v in Y and
A12: z = g . v by FUNCT_1:def_6;
reconsider v = v as Element of L2 by A10;
v in compactbelow (f . (g . y)) by A11;
then v in compactbelow y by A3, A6, FUNCT_1:35;
then v <= y by WAYBEL_8:4;
then A13: g . v <= g . y by A4, WAYBEL_0:66;
v is compact by A11, WAYBEL_8:4;
then g . v is compact by A2, A4, A7, Th28;
hence z in compactbelow (g . y) by A12, A13, WAYBEL_8:4; ::_thesis: verum
end;
then reconsider X = g .: Y as finite Subset of (compactbelow (g . y)) by TARSKI:def_3;
consider x being Element of L1 such that
A14: x in compactbelow (g . y) and
A15: x is_>=_than X by A8, WAYBEL_0:1;
take fx = f . x; ::_thesis: ( fx in compactbelow (f . (g . y)) & fx is_>=_than Y )
x <= g . y by A14, WAYBEL_8:4;
then A16: f . x <= f . (g . y) by A3, WAYBEL_0:66;
x is compact by A14, WAYBEL_8:4;
then f . x is compact by A2, A3, A7, Th28;
hence fx in compactbelow (f . (g . y)) by A16, WAYBEL_8:4; ::_thesis: fx is_>=_than Y
f .: X = f .: (f " Y) by A3, FUNCT_1:85
.= Y by A9, FUNCT_1:77 ;
hence fx is_>=_than Y by A3, A15, Th19; ::_thesis: verum
end;
then ( not compactbelow (f . (g . y)) is empty & compactbelow (f . (g . y)) is directed ) by WAYBEL_0:1;
hence ( not compactbelow y is empty & compactbelow y is directed ) by A3, A6, FUNCT_1:35; ::_thesis: verum
end;
( L2 is up-complete & L2 is satisfying_axiom_K ) by A1, A2, Th30, Th31;
hence L2 is algebraic by A5, WAYBEL_8:def_4; ::_thesis: verum
end;
Lm5: for L being LATTICE st ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) holds
L is algebraic
proof
let L be LATTICE; ::_thesis: ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic )
given X being set , c being closure Function of (BoolePoset X),(BoolePoset X) such that A1: c is directed-sups-preserving and
A2: L, Image c are_isomorphic ; ::_thesis: L is algebraic
( Image c is complete LATTICE & Image c is algebraic LATTICE ) by A1, WAYBEL_8:24, YELLOW_2:35;
hence L is algebraic by A2, Th32, WAYBEL_1:6; ::_thesis: verum
end;
theorem :: WAYBEL13:33
for L being lower-bounded continuous sup-Semilattice holds
( SupMap L is infs-preserving & SupMap L is sups-preserving ) by WAYBEL_1:12, WAYBEL_1:57, WAYBEL_5:3;
theorem :: WAYBEL13:34
for L being lower-bounded LATTICE holds
( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) )
proof
let L be lower-bounded LATTICE; ::_thesis: ( ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) & ( ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) )
thus ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ) by Lm1; ::_thesis: ( ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic )
thus ( ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic ) ::_thesis: verum
proof
assume ex X being set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) ; ::_thesis: L is algebraic
then ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) by Lm3;
hence L is algebraic by Lm5; ::_thesis: verum
end;
end;
theorem :: WAYBEL13:35
for L being lower-bounded LATTICE holds
( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) )
proof
let L be lower-bounded LATTICE; ::_thesis: ( ( L is algebraic implies ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) ) & ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) )
hereby ::_thesis: ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic )
assume L is algebraic ; ::_thesis: ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic )
then ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) by Lm1;
hence ex X being non empty set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) by Lm2; ::_thesis: verum
end;
thus ( ex X being set ex c being closure Function of (BoolePoset X),(BoolePoset X) st
( c is directed-sups-preserving & L, Image c are_isomorphic ) implies L is algebraic ) by Lm5; ::_thesis: verum
end;