:: WAYBEL_7 semantic presentation
begin
theorem Th1: :: WAYBEL_7:1
for L being complete LATTICE
for X, Y being set st X c= Y holds
( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) )
proof
let L be complete LATTICE; ::_thesis: for X, Y being set st X c= Y holds
( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) )
let X, Y be set ; ::_thesis: ( X c= Y implies ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) )
A1: ( ex_inf_of X,L & ex_inf_of Y,L ) by YELLOW_0:17;
( ex_sup_of X,L & ex_sup_of Y,L ) by YELLOW_0:17;
hence ( X c= Y implies ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) ) by A1, YELLOW_0:34, YELLOW_0:35; ::_thesis: verum
end;
theorem Th2: :: WAYBEL_7:2
for X being set holds the carrier of (BoolePoset X) = bool X
proof
let X be set ; ::_thesis: the carrier of (BoolePoset X) = bool X
set L = BoolePoset X;
BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
then BoolePoset X = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def_1;
hence the carrier of (BoolePoset X) = bool X ; ::_thesis: verum
end;
theorem Th3: :: WAYBEL_7:3
for L being non empty antisymmetric bounded RelStr holds
( L is trivial iff Top L = Bottom L )
proof
let L be non empty antisymmetric bounded RelStr ; ::_thesis: ( L is trivial iff Top L = Bottom L )
thus ( L is trivial implies Top L = Bottom L ) by STRUCT_0:def_10; ::_thesis: ( Top L = Bottom L implies L is trivial )
assume A1: Top L = Bottom L ; ::_thesis: L is trivial
let x, y be Element of L; :: according to STRUCT_0:def_10 ::_thesis: x = y
reconsider x = x, y = y as Element of L ;
( x >= Bottom L & x <= Bottom L ) by A1, YELLOW_0:44, YELLOW_0:45;
then A2: x = Bottom L by ORDERS_2:2;
( y >= Bottom L & y <= Bottom L ) by A1, YELLOW_0:44, YELLOW_0:45;
hence x = y by A2, ORDERS_2:2; ::_thesis: verum
end;
registration
let X be set ;
cluster BoolePoset X -> Boolean ;
coherence
BoolePoset X is Boolean ;
end;
registration
let X be non empty set ;
cluster BoolePoset X -> non trivial ;
coherence
not BoolePoset X is trivial
proof
( Top (BoolePoset X) = X & Bottom (BoolePoset X) = {} ) by YELLOW_1:18, YELLOW_1:19;
hence not BoolePoset X is trivial by Th3; ::_thesis: verum
end;
end;
theorem Th4: :: WAYBEL_7:4
for L being non empty lower-bounded Poset
for F being Filter of L holds
( F is proper iff not Bottom L in F )
proof
let L be non empty lower-bounded Poset; ::_thesis: for F being Filter of L holds
( F is proper iff not Bottom L in F )
let F be Filter of L; ::_thesis: ( F is proper iff not Bottom L in F )
hereby ::_thesis: ( not Bottom L in F implies F is proper )
assume F is proper ; ::_thesis: not Bottom L in F
then F <> the carrier of L by SUBSET_1:def_6;
then consider a being set such that
A1: ( ( a in F & not a in the carrier of L ) or ( a in the carrier of L & not a in F ) ) by TARSKI:1;
reconsider a = a as Element of L by A1;
a >= Bottom L by YELLOW_0:44;
hence not Bottom L in F by A1, WAYBEL_0:def_20; ::_thesis: verum
end;
assume not Bottom L in F ; ::_thesis: F is proper
then F <> the carrier of L ;
hence F is proper by SUBSET_1:def_6; ::_thesis: verum
end;
registration
cluster non empty non trivial strict reflexive transitive antisymmetric Boolean non void with_suprema with_infima for RelStr ;
existence
ex b1 being LATTICE st
( not b1 is trivial & b1 is Boolean & b1 is strict )
proof
take BoolePoset {{}} ; ::_thesis: ( not BoolePoset {{}} is trivial & BoolePoset {{}} is Boolean & BoolePoset {{}} is strict )
thus ( not BoolePoset {{}} is trivial & BoolePoset {{}} is Boolean & BoolePoset {{}} is strict ) ; ::_thesis: verum
end;
end;
registration
let L be non trivial upper-bounded Poset;
cluster non empty proper filtered upper for Element of bool the carrier of L;
existence
ex b1 being Filter of L st b1 is proper
proof
take F = uparrow (Top L); ::_thesis: F is proper
assume not F is proper ; ::_thesis: contradiction
then A1: F = the carrier of L by SUBSET_1:def_6;
now__::_thesis:_for_x,_y_being_Element_of_L_holds_x_=_y
let x, y be Element of L; ::_thesis: x = y
A2: F = {(Top L)} by WAYBEL_4:24;
then x = Top L by A1, TARSKI:def_1;
hence x = y by A1, A2, TARSKI:def_1; ::_thesis: verum
end;
hence contradiction by STRUCT_0:def_10; ::_thesis: verum
end;
end;
theorem Th5: :: WAYBEL_7:5
for X being set
for a being Element of (BoolePoset X) holds 'not' a = X \ a
proof
let X be set ; ::_thesis: for a being Element of (BoolePoset X) holds 'not' a = X \ a
let a be Element of (BoolePoset X); ::_thesis: 'not' a = X \ a
A1: the carrier of (BoolePoset X) = bool X by Th2;
reconsider b = X \ a as Element of (BoolePoset X) by Th2;
A2: a misses b by XBOOLE_1:79;
A3: a "/\" b = a /\ b by YELLOW_1:17
.= {} by A2, XBOOLE_0:def_7
.= Bottom (BoolePoset X) by YELLOW_1:18 ;
a "\/" b = a \/ b by YELLOW_1:17
.= X by A1, XBOOLE_1:45
.= Top (BoolePoset X) by YELLOW_1:19 ;
then b is_a_complement_of a by A3, WAYBEL_1:def_23;
hence 'not' a = X \ a by YELLOW_5:11; ::_thesis: verum
end;
theorem :: WAYBEL_7:6
for X being set
for Y being Subset of (BoolePoset X) holds
( Y is lower iff for x, y being set st x c= y & y in Y holds
x in Y )
proof
let X be set ; ::_thesis: for Y being Subset of (BoolePoset X) holds
( Y is lower iff for x, y being set st x c= y & y in Y holds
x in Y )
let Y be Subset of (BoolePoset X); ::_thesis: ( Y is lower iff for x, y being set st x c= y & y in Y holds
x in Y )
A1: the carrier of (BoolePoset X) = bool X by Th2;
hereby ::_thesis: ( ( for x, y being set st x c= y & y in Y holds
x in Y ) implies Y is lower )
assume A2: Y is lower ; ::_thesis: for x, y being set st x c= y & y in Y holds
x in Y
let x, y be set ; ::_thesis: ( x c= y & y in Y implies x in Y )
assume that
A3: x c= y and
A4: y in Y ; ::_thesis: x in Y
reconsider a = x, b = y as Element of (BoolePoset X) by A1, A3, A4, XBOOLE_1:1;
a <= b by A3, YELLOW_1:2;
hence x in Y by A2, A4, WAYBEL_0:def_19; ::_thesis: verum
end;
assume A5: for x, y being set st x c= y & y in Y holds
x in Y ; ::_thesis: Y is lower
let a, b be Element of (BoolePoset X); :: according to WAYBEL_0:def_19 ::_thesis: ( not a in Y or not b <= a or b in Y )
assume that
A6: a in Y and
A7: b <= a ; ::_thesis: b in Y
b c= a by A7, YELLOW_1:2;
hence b in Y by A5, A6; ::_thesis: verum
end;
theorem Th7: :: WAYBEL_7:7
for X being set
for Y being Subset of (BoolePoset X) holds
( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds
y in Y )
proof
let X be set ; ::_thesis: for Y being Subset of (BoolePoset X) holds
( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds
y in Y )
let Y be Subset of (BoolePoset X); ::_thesis: ( Y is upper iff for x, y being set st x c= y & y c= X & x in Y holds
y in Y )
A1: the carrier of (BoolePoset X) = bool X by Th2;
hereby ::_thesis: ( ( for x, y being set st x c= y & y c= X & x in Y holds
y in Y ) implies Y is upper )
assume A2: Y is upper ; ::_thesis: for x, y being set st x c= y & y c= X & x in Y holds
y in Y
let x, y be set ; ::_thesis: ( x c= y & y c= X & x in Y implies y in Y )
assume that
A3: x c= y and
A4: y c= X and
A5: x in Y ; ::_thesis: y in Y
reconsider a = x, b = y as Element of (BoolePoset X) by A4, A5, Th2;
a <= b by A3, YELLOW_1:2;
hence y in Y by A2, A5, WAYBEL_0:def_20; ::_thesis: verum
end;
assume A6: for x, y being set st x c= y & y c= X & x in Y holds
y in Y ; ::_thesis: Y is upper
let a, b be Element of (BoolePoset X); :: according to WAYBEL_0:def_20 ::_thesis: ( not a in Y or not a <= b or b in Y )
assume that
A7: a in Y and
A8: b >= a ; ::_thesis: b in Y
a c= b by A8, YELLOW_1:2;
hence b in Y by A1, A6, A7; ::_thesis: verum
end;
theorem :: WAYBEL_7:8
for X being set
for Y being lower Subset of (BoolePoset X) holds
( Y is directed iff for x, y being set st x in Y & y in Y holds
x \/ y in Y )
proof
let X be set ; ::_thesis: for Y being lower Subset of (BoolePoset X) holds
( Y is directed iff for x, y being set st x in Y & y in Y holds
x \/ y in Y )
let Y be lower Subset of (BoolePoset X); ::_thesis: ( Y is directed iff for x, y being set st x in Y & y in Y holds
x \/ y in Y )
hereby ::_thesis: ( ( for x, y being set st x in Y & y in Y holds
x \/ y in Y ) implies Y is directed )
assume A1: Y is directed ; ::_thesis: for x, y being set st x in Y & y in Y holds
x \/ y in Y
let x, y be set ; ::_thesis: ( x in Y & y in Y implies x \/ y in Y )
assume A2: ( x in Y & y in Y ) ; ::_thesis: x \/ y in Y
then reconsider a = x, b = y as Element of (BoolePoset X) ;
a "\/" b in Y by A1, A2, WAYBEL_0:40;
hence x \/ y in Y by YELLOW_1:17; ::_thesis: verum
end;
assume A3: for x, y being set st x in Y & y in Y holds
x \/ y in Y ; ::_thesis: Y is directed
now__::_thesis:_for_a,_b_being_Element_of_(BoolePoset_X)_st_a_in_Y_&_b_in_Y_holds_
a_"\/"_b_in_Y
let a, b be Element of (BoolePoset X); ::_thesis: ( a in Y & b in Y implies a "\/" b in Y )
assume ( a in Y & b in Y ) ; ::_thesis: a "\/" b in Y
then a \/ b in Y by A3;
hence a "\/" b in Y by YELLOW_1:17; ::_thesis: verum
end;
hence Y is directed by WAYBEL_0:40; ::_thesis: verum
end;
theorem Th9: :: WAYBEL_7:9
for X being set
for Y being upper Subset of (BoolePoset X) holds
( Y is filtered iff for x, y being set st x in Y & y in Y holds
x /\ y in Y )
proof
let X be set ; ::_thesis: for Y being upper Subset of (BoolePoset X) holds
( Y is filtered iff for x, y being set st x in Y & y in Y holds
x /\ y in Y )
let Y be upper Subset of (BoolePoset X); ::_thesis: ( Y is filtered iff for x, y being set st x in Y & y in Y holds
x /\ y in Y )
hereby ::_thesis: ( ( for x, y being set st x in Y & y in Y holds
x /\ y in Y ) implies Y is filtered )
assume A1: Y is filtered ; ::_thesis: for x, y being set st x in Y & y in Y holds
x /\ y in Y
let x, y be set ; ::_thesis: ( x in Y & y in Y implies x /\ y in Y )
assume A2: ( x in Y & y in Y ) ; ::_thesis: x /\ y in Y
then reconsider a = x, b = y as Element of (BoolePoset X) ;
a "/\" b in Y by A1, A2, WAYBEL_0:41;
hence x /\ y in Y by YELLOW_1:17; ::_thesis: verum
end;
assume A3: for x, y being set st x in Y & y in Y holds
x /\ y in Y ; ::_thesis: Y is filtered
now__::_thesis:_for_a,_b_being_Element_of_(BoolePoset_X)_st_a_in_Y_&_b_in_Y_holds_
a_"/\"_b_in_Y
let a, b be Element of (BoolePoset X); ::_thesis: ( a in Y & b in Y implies a "/\" b in Y )
assume ( a in Y & b in Y ) ; ::_thesis: a "/\" b in Y
then a /\ b in Y by A3;
hence a "/\" b in Y by YELLOW_1:17; ::_thesis: verum
end;
hence Y is filtered by WAYBEL_0:41; ::_thesis: verum
end;
theorem :: WAYBEL_7:10
for X being set
for Y being non empty lower Subset of (BoolePoset X) holds
( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y )
proof
let X be set ; ::_thesis: for Y being non empty lower Subset of (BoolePoset X) holds
( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y )
let Y be non empty lower Subset of (BoolePoset X); ::_thesis: ( Y is directed iff for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y )
hereby ::_thesis: ( ( for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y ) implies Y is directed )
assume A1: Y is directed ; ::_thesis: for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y
let Z be finite Subset-Family of X; ::_thesis: ( Z c= Y implies union Z in Y )
reconsider B = Z as Subset of (BoolePoset X) by Th2;
assume Z c= Y ; ::_thesis: union Z in Y
then reconsider A = Z as finite Subset of Y ;
A2: ( A <> {} implies sup B in Y ) by A1, WAYBEL_0:42;
Bottom (BoolePoset X) in Y by A1, WAYBEL_4:21;
hence union Z in Y by A2, YELLOW_1:18, YELLOW_1:21, ZFMISC_1:2; ::_thesis: verum
end;
assume A3: for Z being finite Subset-Family of X st Z c= Y holds
union Z in Y ; ::_thesis: Y is directed
A4: the carrier of (BoolePoset X) = bool X by Th2;
now__::_thesis:_for_A_being_finite_Subset_of_Y_st_A_<>_{}_holds_
"\/"_(A,(BoolePoset_X))_in_Y
let A be finite Subset of Y; ::_thesis: ( A <> {} implies "\/" (A,(BoolePoset X)) in Y )
reconsider Z = A as finite Subset-Family of X by A4, XBOOLE_1:1;
assume A <> {} ; ::_thesis: "\/" (A,(BoolePoset X)) in Y
reconsider Z = Z as finite Subset-Family of X ;
A c= the carrier of (BoolePoset X) by XBOOLE_1:1;
then union Z = "\/" (A,(BoolePoset X)) by YELLOW_1:21;
hence "\/" (A,(BoolePoset X)) in Y by A3; ::_thesis: verum
end;
hence Y is directed by WAYBEL_0:42; ::_thesis: verum
end;
theorem Th11: :: WAYBEL_7:11
for X being set
for Y being non empty upper Subset of (BoolePoset X) holds
( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y )
proof
let X be set ; ::_thesis: for Y being non empty upper Subset of (BoolePoset X) holds
( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y )
let Y be non empty upper Subset of (BoolePoset X); ::_thesis: ( Y is filtered iff for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y )
hereby ::_thesis: ( ( for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y ) implies Y is filtered )
assume A1: Y is filtered ; ::_thesis: for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y
then Top (BoolePoset X) in Y by WAYBEL_4:22;
then A2: X in Y by YELLOW_1:19;
let Z be finite Subset-Family of X; ::_thesis: ( Z c= Y implies Intersect Z in Y )
reconsider B = Z as Subset of (BoolePoset X) by Th2;
assume Z c= Y ; ::_thesis: Intersect Z in Y
then reconsider A = Z as finite Subset of Y ;
( A <> {} implies ( inf B in Y & inf B = meet B ) ) by A1, WAYBEL_0:43, YELLOW_1:20;
hence Intersect Z in Y by A2, SETFAM_1:def_9; ::_thesis: verum
end;
assume A3: for Z being finite Subset-Family of X st Z c= Y holds
Intersect Z in Y ; ::_thesis: Y is filtered
A4: the carrier of (BoolePoset X) = bool X by Th2;
now__::_thesis:_for_A_being_finite_Subset_of_Y_st_A_<>_{}_holds_
"/\"_(A,(BoolePoset_X))_in_Y
let A be finite Subset of Y; ::_thesis: ( A <> {} implies "/\" (A,(BoolePoset X)) in Y )
reconsider Z = A as finite Subset-Family of X by A4, XBOOLE_1:1;
assume A5: A <> {} ; ::_thesis: "/\" (A,(BoolePoset X)) in Y
reconsider Z = Z as finite Subset-Family of X ;
A c= the carrier of (BoolePoset X) by XBOOLE_1:1;
then "/\" (A,(BoolePoset X)) = meet Z by A5, YELLOW_1:20
.= Intersect Z by A5, SETFAM_1:def_9 ;
hence "/\" (A,(BoolePoset X)) in Y by A3; ::_thesis: verum
end;
hence Y is filtered by WAYBEL_0:43; ::_thesis: verum
end;
begin
definition
let L be with_infima Poset;
let I be Ideal of L;
attrI is prime means :Def1: :: WAYBEL_7:def 1
for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I );
end;
:: deftheorem Def1 defines prime WAYBEL_7:def_1_:_
for L being with_infima Poset
for I being Ideal of L holds
( I is prime iff for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) );
theorem Th12: :: WAYBEL_7:12
for L being with_infima Poset
for I being Ideal of L holds
( I is prime iff for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) )
proof
let L be with_infima Poset; ::_thesis: for I being Ideal of L holds
( I is prime iff for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) )
let I be Ideal of L; ::_thesis: ( I is prime iff for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) )
thus ( I is prime implies for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) ) ::_thesis: ( ( for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) ) implies I is prime )
proof
defpred S1[ set ] means ( not $1 is empty & "/\" ($1,L) in I implies ex a being Element of L st
( a in $1 & a in I ) );
assume A1: for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_1 ::_thesis: for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I )
let A be non empty finite Subset of L; ::_thesis: ( inf A in I implies ex a being Element of L st
( a in A & a in I ) )
A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in A and
A4: B c= A and
A5: S1[B] ; ::_thesis: S1[B \/ {x}]
thus S1[B \/ {x}] ::_thesis: verum
proof
reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by A4, XBOOLE_1:1;
assume that
not B \/ {x} is empty and
A6: "/\" ((B \/ {x}),L) in I ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
then ( "/\" ((B \/ {a}),L) = a & a in B \/ {a} ) by TARSKI:def_1, YELLOW_0:39;
hence ex a being Element of L st
( a in B \/ {x} & a in I ) by A6; ::_thesis: verum
end;
supposeA7: B <> {} ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
A8: inf {a} = a by YELLOW_0:39;
A9: ex_inf_of {a},L by YELLOW_0:55;
ex_inf_of C,L by A7, YELLOW_0:55;
then A10: "/\" ((B \/ {x}),L) = (inf C) "/\" (inf {a}) by A9, YELLOW_2:4;
hereby ::_thesis: verum
percases ( inf C in I or a in I ) by A1, A6, A10, A8;
suppose inf C in I ; ::_thesis: ex b being Element of L st
( b in B \/ {x} & b in I )
then consider b being Element of L such that
A11: ( b in B & b in I ) by A5, A7;
take b = b; ::_thesis: ( b in B \/ {x} & b in I )
thus ( b in B \/ {x} & b in I ) by A11, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA12: a in I ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
take a = a; ::_thesis: ( a in B \/ {x} & a in I )
a in {a} by TARSKI:def_1;
hence ( a in B \/ {x} & a in I ) by A12, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
A13: S1[ {} ] ;
A14: A is finite ;
S1[A] from FINSET_1:sch_2(A14, A13, A2);
hence ( inf A in I implies ex a being Element of L st
( a in A & a in I ) ) ; ::_thesis: verum
end;
assume A15: for A being non empty finite Subset of L st inf A in I holds
ex a being Element of L st
( a in A & a in I ) ; ::_thesis: I is prime
let a, b be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not a "/\" b in I or a in I or b in I )
assume a "/\" b in I ; ::_thesis: ( a in I or b in I )
then inf {a,b} in I by YELLOW_0:40;
then ex x being Element of L st
( x in {a,b} & x in I ) by A15;
hence ( a in I or b in I ) by TARSKI:def_2; ::_thesis: verum
end;
registration
let L be LATTICE;
cluster non empty directed lower prime for Element of bool the carrier of L;
existence
ex b1 being Ideal of L st b1 is prime
proof
take [#] L ; ::_thesis: [#] L is prime
let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in [#] L or x in [#] L or y in [#] L )
thus ( not x "/\" y in [#] L or x in [#] L or y in [#] L ) ; ::_thesis: verum
end;
end;
theorem :: WAYBEL_7:13
for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for x being set st x is prime Ideal of L1 holds
x is prime Ideal of L2
proof
let L1, L2 be LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being set st x is prime Ideal of L1 holds
x is prime Ideal of L2 )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for x being set st x is prime Ideal of L1 holds
x is prime Ideal of L2
let x be set ; ::_thesis: ( x is prime Ideal of L1 implies x is prime Ideal of L2 )
assume x is prime Ideal of L1 ; ::_thesis: x is prime Ideal of L2
then reconsider I = x as prime Ideal of L1 ;
reconsider I9 = I as Subset of L2 by A1;
reconsider I9 = I9 as Ideal of L2 by A1, WAYBEL_0:3, WAYBEL_0:25;
I9 is prime
proof
let x, y be Element of L2; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in I9 or x in I9 or y in I9 )
reconsider a = x, b = y as Element of L1 by A1;
A2: x "/\" y = inf {x,y} by YELLOW_0:40;
( ex_inf_of {a,b},L1 & a "/\" b = inf {a,b} ) by YELLOW_0:21, YELLOW_0:40;
then a "/\" b = x "/\" y by A1, A2, YELLOW_0:27;
hence ( not x "/\" y in I9 or x in I9 or y in I9 ) by Def1; ::_thesis: verum
end;
hence x is prime Ideal of L2 ; ::_thesis: verum
end;
definition
let L be with_suprema Poset;
let F be Filter of L;
attrF is prime means :Def2: :: WAYBEL_7:def 2
for x, y being Element of L holds
( not x "\/" y in F or x in F or y in F );
end;
:: deftheorem Def2 defines prime WAYBEL_7:def_2_:_
for L being with_suprema Poset
for F being Filter of L holds
( F is prime iff for x, y being Element of L holds
( not x "\/" y in F or x in F or y in F ) );
theorem :: WAYBEL_7:14
for L being with_suprema Poset
for F being Filter of L holds
( F is prime iff for A being non empty finite Subset of L st sup A in F holds
ex a being Element of L st
( a in A & a in F ) )
proof
let L be with_suprema Poset; ::_thesis: for F being Filter of L holds
( F is prime iff for A being non empty finite Subset of L st sup A in F holds
ex a being Element of L st
( a in A & a in F ) )
let I be Filter of L; ::_thesis: ( I is prime iff for A being non empty finite Subset of L st sup A in I holds
ex a being Element of L st
( a in A & a in I ) )
thus ( I is prime implies for A being non empty finite Subset of L st sup A in I holds
ex a being Element of L st
( a in A & a in I ) ) ::_thesis: ( ( for A being non empty finite Subset of L st sup A in I holds
ex a being Element of L st
( a in A & a in I ) ) implies I is prime )
proof
defpred S1[ set ] means ( not $1 is empty & "\/" ($1,L) in I implies ex a being Element of L st
( a in $1 & a in I ) );
assume A1: for x, y being Element of L holds
( not x "\/" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_2 ::_thesis: for A being non empty finite Subset of L st sup A in I holds
ex a being Element of L st
( a in A & a in I )
let A be non empty finite Subset of L; ::_thesis: ( sup A in I implies ex a being Element of L st
( a in A & a in I ) )
A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in A and
A4: B c= A and
A5: S1[B] ; ::_thesis: S1[B \/ {x}]
thus S1[B \/ {x}] ::_thesis: verum
proof
reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by A4, XBOOLE_1:1;
assume that
not B \/ {x} is empty and
A6: "\/" ((B \/ {x}),L) in I ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
then ( "\/" ((B \/ {a}),L) = a & a in B \/ {a} ) by TARSKI:def_1, YELLOW_0:39;
hence ex a being Element of L st
( a in B \/ {x} & a in I ) by A6; ::_thesis: verum
end;
supposeA7: B <> {} ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
A8: sup {a} = a by YELLOW_0:39;
A9: ex_sup_of {a},L by YELLOW_0:54;
ex_sup_of C,L by A7, YELLOW_0:54;
then A10: "\/" ((B \/ {x}),L) = (sup C) "\/" (sup {a}) by A9, YELLOW_2:3;
hereby ::_thesis: verum
percases ( sup C in I or a in I ) by A1, A6, A10, A8;
suppose sup C in I ; ::_thesis: ex b being Element of L st
( b in B \/ {x} & b in I )
then consider b being Element of L such that
A11: ( b in B & b in I ) by A5, A7;
take b = b; ::_thesis: ( b in B \/ {x} & b in I )
thus ( b in B \/ {x} & b in I ) by A11, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA12: a in I ; ::_thesis: ex a being Element of L st
( a in B \/ {x} & a in I )
take a = a; ::_thesis: ( a in B \/ {x} & a in I )
a in {a} by TARSKI:def_1;
hence ( a in B \/ {x} & a in I ) by A12, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
A13: S1[ {} ] ;
A14: A is finite ;
S1[A] from FINSET_1:sch_2(A14, A13, A2);
hence ( sup A in I implies ex a being Element of L st
( a in A & a in I ) ) ; ::_thesis: verum
end;
assume A15: for A being non empty finite Subset of L st sup A in I holds
ex a being Element of L st
( a in A & a in I ) ; ::_thesis: I is prime
let a, b be Element of L; :: according to WAYBEL_7:def_2 ::_thesis: ( not a "\/" b in I or a in I or b in I )
assume a "\/" b in I ; ::_thesis: ( a in I or b in I )
then sup {a,b} in I by YELLOW_0:41;
then ex x being Element of L st
( x in {a,b} & x in I ) by A15;
hence ( a in I or b in I ) by TARSKI:def_2; ::_thesis: verum
end;
registration
let L be LATTICE;
cluster non empty filtered upper prime for Element of bool the carrier of L;
existence
ex b1 being Filter of L st b1 is prime
proof
take [#] L ; ::_thesis: [#] L is prime
let x, y be Element of L; :: according to WAYBEL_7:def_2 ::_thesis: ( not x "\/" y in [#] L or x in [#] L or y in [#] L )
thus ( not x "\/" y in [#] L or x in [#] L or y in [#] L ) ; ::_thesis: verum
end;
end;
theorem Th15: :: WAYBEL_7:15
for L1, L2 being LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for x being set st x is prime Filter of L1 holds
x is prime Filter of L2
proof
let L1, L2 be LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for x being set st x is prime Filter of L1 holds
x is prime Filter of L2 )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for x being set st x is prime Filter of L1 holds
x is prime Filter of L2
let x be set ; ::_thesis: ( x is prime Filter of L1 implies x is prime Filter of L2 )
assume x is prime Filter of L1 ; ::_thesis: x is prime Filter of L2
then reconsider I = x as prime Filter of L1 ;
reconsider I9 = I as Subset of L2 by A1;
reconsider I9 = I9 as Filter of L2 by A1, WAYBEL_0:4, WAYBEL_0:25;
I9 is prime
proof
let x, y be Element of L2; :: according to WAYBEL_7:def_2 ::_thesis: ( not x "\/" y in I9 or x in I9 or y in I9 )
reconsider a = x, b = y as Element of L1 by A1;
A2: x "\/" y = sup {x,y} by YELLOW_0:41;
( ex_sup_of {a,b},L1 & a "\/" b = sup {a,b} ) by YELLOW_0:20, YELLOW_0:41;
then a "\/" b = x "\/" y by A1, A2, YELLOW_0:26;
hence ( not x "\/" y in I9 or x in I9 or y in I9 ) by Def2; ::_thesis: verum
end;
hence x is prime Filter of L2 ; ::_thesis: verum
end;
theorem Th16: :: WAYBEL_7:16
for L being LATTICE
for x being set holds
( x is prime Ideal of L iff x is prime Filter of (L opp) )
proof
let L be LATTICE; ::_thesis: for x being set holds
( x is prime Ideal of L iff x is prime Filter of (L opp) )
let x be set ; ::_thesis: ( x is prime Ideal of L iff x is prime Filter of (L opp) )
hereby ::_thesis: ( x is prime Filter of (L opp) implies x is prime Ideal of L )
assume x is prime Ideal of L ; ::_thesis: x is prime Filter of (L opp)
then reconsider I = x as prime Ideal of L ;
reconsider F = I as Filter of (L opp) by YELLOW_7:26, YELLOW_7:28;
F is prime
proof
let x, y be Element of (L opp); :: according to WAYBEL_7:def_2 ::_thesis: ( not x "\/" y in F or x in F or y in F )
A1: x "\/" y = (~ x) "/\" (~ y) by YELLOW_7:22;
( ~ x = x & ~ y = y ) by LATTICE3:def_7;
hence ( not x "\/" y in F or x in F or y in F ) by A1, Def1; ::_thesis: verum
end;
hence x is prime Filter of (L opp) ; ::_thesis: verum
end;
assume x is prime Filter of (L opp) ; ::_thesis: x is prime Ideal of L
then reconsider I = x as prime Filter of (L opp) ;
reconsider F = I as Ideal of L by YELLOW_7:26, YELLOW_7:28;
F is prime
proof
let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in F or x in F or y in F )
A2: x "/\" y = (x ~) "\/" (y ~) by YELLOW_7:21;
( x ~ = x & y ~ = y ) by LATTICE3:def_6;
hence ( not x "/\" y in F or x in F or y in F ) by A2, Def2; ::_thesis: verum
end;
hence x is prime Ideal of L ; ::_thesis: verum
end;
theorem Th17: :: WAYBEL_7:17
for L being LATTICE
for x being set holds
( x is prime Filter of L iff x is prime Ideal of (L opp) )
proof
let L be LATTICE; ::_thesis: for x being set holds
( x is prime Filter of L iff x is prime Ideal of (L opp) )
let x be set ; ::_thesis: ( x is prime Filter of L iff x is prime Ideal of (L opp) )
(L opp) opp = RelStr(# the carrier of L, the InternalRel of L #) by LATTICE3:8;
then ( x is prime Filter of L iff x is prime Filter of ((L opp) opp) ) by Th15;
hence ( x is prime Filter of L iff x is prime Ideal of (L opp) ) by Th16; ::_thesis: verum
end;
theorem :: WAYBEL_7:18
for L being with_infima Poset
for I being Ideal of L holds
( I is prime iff ( I ` is Filter of L or I ` = {} ) )
proof
let L be with_infima Poset; ::_thesis: for I being Ideal of L holds
( I is prime iff ( I ` is Filter of L or I ` = {} ) )
let I be Ideal of L; ::_thesis: ( I is prime iff ( I ` is Filter of L or I ` = {} ) )
set F = I ` ;
thus ( not I is prime or I ` is Filter of L or I ` = {} ) ::_thesis: ( ( I ` is Filter of L or I ` = {} ) implies I is prime )
proof
assume A1: for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_1 ::_thesis: ( I ` is Filter of L or I ` = {} )
A2: I ` is filtered
proof
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in I ` or not y in I ` or ex b1 being Element of the carrier of L st
( b1 in I ` & b1 <= x & b1 <= y ) )
assume ( x in I ` & y in I ` ) ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in I ` & b1 <= x & b1 <= y )
then ( not x in I & not y in I ) by XBOOLE_0:def_5;
then A3: x "/\" y in I ` by A1, SUBSET_1:29;
( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
hence ex b1 being Element of the carrier of L st
( b1 in I ` & b1 <= x & b1 <= y ) by A3; ::_thesis: verum
end;
I ` is upper
proof
let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in I ` or not x <= y or y in I ` )
assume that
A4: x in I ` and
A5: y >= x ; ::_thesis: y in I `
( y in I implies x in I ) by A5, WAYBEL_0:def_19;
hence y in I ` by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( I ` is Filter of L or I ` = {} ) by A2; ::_thesis: verum
end;
assume A6: ( I ` is Filter of L or I ` = {} ) ; ::_thesis: I is prime
let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in I or x in I or y in I )
assume x "/\" y in I ; ::_thesis: ( x in I or y in I )
then not x "/\" y in I ` by XBOOLE_0:def_5;
then ( not x in I ` or not y in I ` ) by A6, WAYBEL_0:41;
hence ( x in I or y in I ) by SUBSET_1:29; ::_thesis: verum
end;
theorem :: WAYBEL_7:19
for L being LATTICE
for I being Ideal of L holds
( I is prime iff I in PRIME (InclPoset (Ids L)) )
proof
let L be LATTICE; ::_thesis: for I being Ideal of L holds
( I is prime iff I in PRIME (InclPoset (Ids L)) )
let I be Ideal of L; ::_thesis: ( I is prime iff I in PRIME (InclPoset (Ids L)) )
set P = InclPoset (Ids L);
A1: InclPoset (Ids L) = RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1;
I in Ids L ;
then reconsider i = I as Element of (InclPoset (Ids L)) by A1;
thus ( I is prime implies I in PRIME (InclPoset (Ids L)) ) ::_thesis: ( I in PRIME (InclPoset (Ids L)) implies I is prime )
proof
assume A2: for x, y being Element of L holds
( not x "/\" y in I or x in I or y in I ) ; :: according to WAYBEL_7:def_1 ::_thesis: I in PRIME (InclPoset (Ids L))
i is prime
proof
let x, y be Element of (InclPoset (Ids L)); :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= i or x <= i or y <= i )
y in Ids L by A1;
then A3: ex J being Ideal of L st y = J ;
x in Ids L by A1;
then ex J being Ideal of L st x = J ;
then reconsider X = x, Y = y as Ideal of L by A3;
assume x "/\" y <= i ; ::_thesis: ( x <= i or y <= i )
then x "/\" y c= I by YELLOW_1:3;
then A4: X /\ Y c= I by YELLOW_2:43;
assume that
A5: not x <= i and
A6: not y <= i ; ::_thesis: contradiction
not X c= I by A5, YELLOW_1:3;
then consider a being set such that
A7: a in X and
A8: not a in I by TARSKI:def_3;
not Y c= I by A6, YELLOW_1:3;
then consider b being set such that
A9: b in Y and
A10: not b in I by TARSKI:def_3;
reconsider a = a, b = b as Element of L by A7, A9;
a "/\" b <= b by YELLOW_0:23;
then A11: a "/\" b in Y by A9, WAYBEL_0:def_19;
a "/\" b <= a by YELLOW_0:23;
then a "/\" b in X by A7, WAYBEL_0:def_19;
then a "/\" b in X /\ Y by A11, XBOOLE_0:def_4;
hence contradiction by A2, A4, A8, A10; ::_thesis: verum
end;
hence I in PRIME (InclPoset (Ids L)) by WAYBEL_6:def_7; ::_thesis: verum
end;
assume A12: I in PRIME (InclPoset (Ids L)) ; ::_thesis: I is prime
let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in I or x in I or y in I )
reconsider X = downarrow x, Y = downarrow y as Ideal of L ;
( X in Ids L & Y in Ids L ) ;
then reconsider X = X, Y = Y as Element of (InclPoset (Ids L)) by A1;
A13: X /\ Y = X "/\" Y by YELLOW_2:43;
assume A14: x "/\" y in I ; ::_thesis: ( x in I or y in I )
X "/\" Y c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X "/\" Y or a in I )
assume A15: a in X "/\" Y ; ::_thesis: a in I
then A16: a in X by A13, XBOOLE_0:def_4;
A17: a in Y by A13, A15, XBOOLE_0:def_4;
reconsider a = a as Element of L by A16;
A18: a <= y by A17, WAYBEL_0:17;
a <= x by A16, WAYBEL_0:17;
then a <= x "/\" y by A18, YELLOW_0:23;
hence a in I by A14, WAYBEL_0:def_19; ::_thesis: verum
end;
then A19: X "/\" Y <= i by YELLOW_1:3;
i is prime by A12, WAYBEL_6:def_7;
then ( X <= i or Y <= i ) by A19, WAYBEL_6:def_6;
then A20: ( X c= I or Y c= I ) by YELLOW_1:3;
y <= y ;
then A21: y in Y by WAYBEL_0:17;
x <= x ;
then x in X by WAYBEL_0:17;
hence ( x in I or y in I ) by A21, A20; ::_thesis: verum
end;
theorem Th20: :: WAYBEL_7:20
for L being Boolean LATTICE
for F being Filter of L holds
( F is prime iff for a being Element of L holds
( a in F or 'not' a in F ) )
proof
let L be Boolean LATTICE; ::_thesis: for F being Filter of L holds
( F is prime iff for a being Element of L holds
( a in F or 'not' a in F ) )
let F be Filter of L; ::_thesis: ( F is prime iff for a being Element of L holds
( a in F or 'not' a in F ) )
hereby ::_thesis: ( ( for a being Element of L holds
( a in F or 'not' a in F ) ) implies F is prime )
assume A1: F is prime ; ::_thesis: for a being Element of L holds
( a in F or 'not' a in F )
let a be Element of L; ::_thesis: ( a in F or 'not' a in F )
set b = 'not' a;
a "\/" ('not' a) = Top L by YELLOW_5:34;
then a "\/" ('not' a) in F by WAYBEL_4:22;
hence ( a in F or 'not' a in F ) by A1, Def2; ::_thesis: verum
end;
assume A2: for a being Element of L holds
( a in F or 'not' a in F ) ; ::_thesis: F is prime
let a, b be Element of L; :: according to WAYBEL_7:def_2 ::_thesis: ( not a "\/" b in F or a in F or b in F )
assume that
A3: a "\/" b in F and
A4: not a in F and
A5: not b in F ; ::_thesis: contradiction
( 'not' a in F & 'not' b in F ) by A2, A4, A5;
then ('not' a) "/\" ('not' b) in F by WAYBEL_0:41;
then 'not' (a "\/" b) in F by YELLOW_5:36;
then ('not' (a "\/" b)) "/\" (a "\/" b) in F by A3, WAYBEL_0:41;
then A6: Bottom L in F by YELLOW_5:34;
a >= Bottom L by YELLOW_0:44;
hence contradiction by A4, A6, WAYBEL_0:def_20; ::_thesis: verum
end;
theorem Th21: :: WAYBEL_7:21
for X being set
for F being Filter of (BoolePoset X) holds
( F is prime iff for A being Subset of X holds
( A in F or X \ A in F ) )
proof
let X be set ; ::_thesis: for F being Filter of (BoolePoset X) holds
( F is prime iff for A being Subset of X holds
( A in F or X \ A in F ) )
set L = BoolePoset X;
let F be Filter of (BoolePoset X); ::_thesis: ( F is prime iff for A being Subset of X holds
( A in F or X \ A in F ) )
BoolePoset X = InclPoset (bool X) by YELLOW_1:4;
then A1: BoolePoset X = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def_1;
hereby ::_thesis: ( ( for A being Subset of X holds
( A in F or X \ A in F ) ) implies F is prime )
assume A2: F is prime ; ::_thesis: for A being Subset of X holds
( A in F or X \ A in F )
let A be Subset of X; ::_thesis: ( A in F or X \ A in F )
reconsider a = A as Element of (BoolePoset X) by A1;
( a in F or 'not' a in F ) by A2, Th20;
hence ( A in F or X \ A in F ) by Th5; ::_thesis: verum
end;
assume A3: for A being Subset of X holds
( A in F or X \ A in F ) ; ::_thesis: F is prime
now__::_thesis:_for_a_being_Element_of_(BoolePoset_X)_holds_
(_a_in_F_or_'not'_a_in_F_)
let a be Element of (BoolePoset X); ::_thesis: ( a in F or 'not' a in F )
'not' a = X \ a by Th5;
hence ( a in F or 'not' a in F ) by A1, A3; ::_thesis: verum
end;
hence F is prime by Th20; ::_thesis: verum
end;
definition
let L be non empty Poset;
let F be Filter of L;
attrF is ultra means :Def3: :: WAYBEL_7:def 3
( F is proper & ( for G being Filter of L holds
( not F c= G or F = G or G = the carrier of L ) ) );
end;
:: deftheorem Def3 defines ultra WAYBEL_7:def_3_:_
for L being non empty Poset
for F being Filter of L holds
( F is ultra iff ( F is proper & ( for G being Filter of L holds
( not F c= G or F = G or G = the carrier of L ) ) ) );
registration
let L be non empty Poset;
cluster non empty filtered upper ultra -> proper for Element of bool the carrier of L;
coherence
for b1 being Filter of L st b1 is ultra holds
b1 is proper by Def3;
end;
Lm1: for L being with_infima Poset
for F being Filter of L
for X being non empty finite Subset of L
for x being Element of L st x in uparrow (fininfs (F \/ X)) holds
ex a being Element of L st
( a in F & x >= a "/\" (inf X) )
proof
let L be with_infima Poset; ::_thesis: for F being Filter of L
for X being non empty finite Subset of L
for x being Element of L st x in uparrow (fininfs (F \/ X)) holds
ex a being Element of L st
( a in F & x >= a "/\" (inf X) )
let I be Filter of L; ::_thesis: for X being non empty finite Subset of L
for x being Element of L st x in uparrow (fininfs (I \/ X)) holds
ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
let X be non empty finite Subset of L; ::_thesis: for x being Element of L st x in uparrow (fininfs (I \/ X)) holds
ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
let x be Element of L; ::_thesis: ( x in uparrow (fininfs (I \/ X)) implies ex a being Element of L st
( a in I & x >= a "/\" (inf X) ) )
set i = the Element of I;
reconsider i = the Element of I as Element of L ;
assume x in uparrow (fininfs (I \/ X)) ; ::_thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
then consider u being Element of L such that
A1: u <= x and
A2: u in fininfs (I \/ X) by WAYBEL_0:def_16;
consider Y being finite Subset of (I \/ X) such that
A3: u = "/\" (Y,L) and
A4: ex_inf_of Y,L by A2;
Y \ X c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y \ X or a in I )
assume A5: a in Y \ X ; ::_thesis: a in I
then not a in X by XBOOLE_0:def_5;
hence a in I by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
then reconsider Z = Y \ X as finite Subset of I ;
reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z9 \/ X as finite Subset of L ;
percases ( Z = {} or Z <> {} ) ;
supposeA6: Z = {} ; ::_thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
A7: inf X >= i "/\" (inf X) by YELLOW_0:23;
take i ; ::_thesis: ( i in I & x >= i "/\" (inf X) )
A8: ex_inf_of X,L by YELLOW_0:55;
Y c= X by A6, XBOOLE_1:37;
then u >= inf X by A3, A4, A8, YELLOW_0:35;
then u >= i "/\" (inf X) by A7, ORDERS_2:3;
hence ( i in I & x >= i "/\" (inf X) ) by A1, ORDERS_2:3; ::_thesis: verum
end;
supposeA9: Z <> {} ; ::_thesis: ex a being Element of L st
( a in I & x >= a "/\" (inf X) )
take inf Z9 ; ::_thesis: ( inf Z9 in I & x >= (inf Z9) "/\" (inf X) )
A10: ex_inf_of X,L by YELLOW_0:55;
A11: ex_inf_of ZX,L by YELLOW_0:55;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z9 \/ X by XBOOLE_1:39;
then A12: inf Y9 >= inf ZX by A4, A11, YELLOW_0:35;
ex_inf_of Z9,L by A9, YELLOW_0:55;
then inf (Z9 \/ X) = (inf Z9) "/\" (inf X) by A10, A11, YELLOW_0:37;
hence ( inf Z9 in I & x >= (inf Z9) "/\" (inf X) ) by A1, A3, A9, A12, ORDERS_2:3, WAYBEL_0:43; ::_thesis: verum
end;
end;
end;
theorem Th22: :: WAYBEL_7:22
for L being Boolean LATTICE
for F being Filter of L holds
( ( F is proper & F is prime ) iff F is ultra )
proof
let L be Boolean LATTICE; ::_thesis: for F being Filter of L holds
( ( F is proper & F is prime ) iff F is ultra )
let F be Filter of L; ::_thesis: ( ( F is proper & F is prime ) iff F is ultra )
thus ( F is proper & F is prime implies F is ultra ) ::_thesis: ( F is ultra implies ( F is proper & F is prime ) )
proof
assume A1: F is proper ; ::_thesis: ( not F is prime or F is ultra )
assume A2: for x, y being Element of L holds
( not x "\/" y in F or x in F or y in F ) ; :: according to WAYBEL_7:def_2 ::_thesis: F is ultra
thus F is proper by A1; :: according to WAYBEL_7:def_3 ::_thesis: for G being Filter of L holds
( not F c= G or F = G or G = the carrier of L )
let G be Filter of L; ::_thesis: ( not F c= G or F = G or G = the carrier of L )
assume that
A3: F c= G and
A4: F <> G ; ::_thesis: G = the carrier of L
consider x being set such that
A5: ( ( x in F & not x in G ) or ( x in G & not x in F ) ) by A4, TARSKI:1;
reconsider x = x as Element of L by A5;
set y = 'not' x;
x "\/" ('not' x) = Top L by YELLOW_5:34;
then 'not' x in F by A2, A3, A5, WAYBEL_4:22;
then x "/\" ('not' x) in G by A3, A5, WAYBEL_0:41;
then A6: Bottom L in G by YELLOW_5:34;
thus G c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= G
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in G )
assume x in the carrier of L ; ::_thesis: x in G
then reconsider x = x as Element of L ;
x >= Bottom L by YELLOW_0:44;
hence x in G by A6, WAYBEL_0:def_20; ::_thesis: verum
end;
assume that
A7: F is proper and
A8: for G being Filter of L holds
( not F c= G or F = G or G = the carrier of L ) ; :: according to WAYBEL_7:def_3 ::_thesis: ( F is proper & F is prime )
thus F is proper by A7; ::_thesis: F is prime
now__::_thesis:_for_a_being_Element_of_L_st_not_a_in_F_holds_
'not'_a_in_F
let a be Element of L; ::_thesis: ( not a in F implies 'not' a in F )
assume that
A9: not a in F and
A10: not 'not' a in F ; ::_thesis: contradiction
set b = 'not' a;
A11: F \/ {a} c= uparrow (fininfs (F \/ {a})) by WAYBEL_0:62;
( {a} c= F \/ {a} & a in {a} ) by TARSKI:def_1, XBOOLE_1:7;
then a in F \/ {a} ;
then ( F c= F \/ {a} & a in uparrow (fininfs (F \/ {a})) ) by A11, XBOOLE_1:7;
then uparrow (fininfs (F \/ {a})) = the carrier of L by A8, A9, A11, XBOOLE_1:1;
then consider c being Element of L such that
A12: c in F and
A13: 'not' a >= c "/\" (inf {a}) by Lm1;
c <= Top L by YELLOW_0:45;
then A14: c = c "/\" (Top L) by YELLOW_0:25
.= c "/\" (a "\/" ('not' a)) by YELLOW_5:34
.= (c "/\" a) "\/" (c "/\" ('not' a)) by WAYBEL_1:def_3 ;
( inf {a} = a & c "/\" ('not' a) <= 'not' a ) by YELLOW_0:23, YELLOW_0:39;
then c <= 'not' a by A13, A14, YELLOW_0:22;
hence contradiction by A10, A12, WAYBEL_0:def_20; ::_thesis: verum
end;
hence F is prime by Th20; ::_thesis: verum
end;
Lm2: for L being with_suprema Poset
for I being Ideal of L
for X being non empty finite Subset of L
for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
proof
let L be with_suprema Poset; ::_thesis: for I being Ideal of L
for X being non empty finite Subset of L
for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
let I be Ideal of L; ::_thesis: for X being non empty finite Subset of L
for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
let X be non empty finite Subset of L; ::_thesis: for x being Element of L st x in downarrow (finsups (I \/ X)) holds
ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
let x be Element of L; ::_thesis: ( x in downarrow (finsups (I \/ X)) implies ex i being Element of L st
( i in I & x <= i "\/" (sup X) ) )
set i = the Element of I;
reconsider i = the Element of I as Element of L ;
assume x in downarrow (finsups (I \/ X)) ; ::_thesis: ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
then consider u being Element of L such that
A1: u >= x and
A2: u in finsups (I \/ X) by WAYBEL_0:def_15;
consider Y being finite Subset of (I \/ X) such that
A3: u = "\/" (Y,L) and
A4: ex_sup_of Y,L by A2;
Y \ X c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y \ X or a in I )
assume A5: a in Y \ X ; ::_thesis: a in I
then not a in X by XBOOLE_0:def_5;
hence a in I by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
then reconsider Z = Y \ X as finite Subset of I ;
reconsider Z9 = Z, Y9 = Y as finite Subset of L by XBOOLE_1:1;
reconsider ZX = Z9 \/ X as finite Subset of L ;
percases ( Z = {} or Z <> {} ) ;
supposeA6: Z = {} ; ::_thesis: ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
A7: sup X <= i "\/" (sup X) by YELLOW_0:22;
take i ; ::_thesis: ( i in I & x <= i "\/" (sup X) )
A8: ex_sup_of X,L by YELLOW_0:54;
Y c= X by A6, XBOOLE_1:37;
then u <= sup X by A3, A4, A8, YELLOW_0:34;
then u <= i "\/" (sup X) by A7, ORDERS_2:3;
hence ( i in I & x <= i "\/" (sup X) ) by A1, ORDERS_2:3; ::_thesis: verum
end;
supposeA9: Z <> {} ; ::_thesis: ex i being Element of L st
( i in I & x <= i "\/" (sup X) )
take sup Z9 ; ::_thesis: ( sup Z9 in I & x <= (sup Z9) "\/" (sup X) )
A10: ex_sup_of X,L by YELLOW_0:54;
A11: ex_sup_of ZX,L by YELLOW_0:54;
Y c= Y \/ X by XBOOLE_1:7;
then Y c= Z9 \/ X by XBOOLE_1:39;
then A12: sup Y9 <= sup ZX by A4, A11, YELLOW_0:34;
ex_sup_of Z9,L by A9, YELLOW_0:54;
then sup (Z9 \/ X) = (sup Z9) "\/" (sup X) by A10, A11, YELLOW_0:36;
hence ( sup Z9 in I & x <= (sup Z9) "\/" (sup X) ) by A1, A3, A9, A12, ORDERS_2:3, WAYBEL_0:42; ::_thesis: verum
end;
end;
end;
theorem Th23: :: WAYBEL_7:23
for L being distributive LATTICE
for I being Ideal of L
for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
proof
let L be distributive LATTICE; ::_thesis: for I being Ideal of L
for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
let I be Ideal of L; ::_thesis: for F being Filter of L st I misses F holds
ex P being Ideal of L st
( P is prime & I c= P & P misses F )
let F be Filter of L; ::_thesis: ( I misses F implies ex P being Ideal of L st
( P is prime & I c= P & P misses F ) )
assume A1: I misses F ; ::_thesis: ex P being Ideal of L st
( P is prime & I c= P & P misses F )
set X = { P where P is Ideal of L : ( I c= P & P misses F ) } ;
A2: now__::_thesis:_for_A_being_set_st_A_in__{__P_where_P_is_Ideal_of_L_:_(_I_c=_P_&_P_misses_F_)__}__holds_
(_I_c=_A_&_A_misses_F_)
let A be set ; ::_thesis: ( A in { P where P is Ideal of L : ( I c= P & P misses F ) } implies ( I c= A & A misses F ) )
assume A in { P where P is Ideal of L : ( I c= P & P misses F ) } ; ::_thesis: ( I c= A & A misses F )
then ex P being Ideal of L st
( A = P & I c= P & P misses F ) ;
hence ( I c= A & A misses F ) ; ::_thesis: verum
end;
A3: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=__{__P_where_P_is_Ideal_of_L_:_(_I_c=_P_&_P_misses_F_)__}__&_Z_is_c=-linear_holds_
union_Z_in__{__P_where_P_is_Ideal_of_L_:_(_I_c=_P_&_P_misses_F_)__}_
let Z be set ; ::_thesis: ( Z <> {} & Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } & Z is c=-linear implies union Z in { P where P is Ideal of L : ( I c= P & P misses F ) } )
assume that
A4: Z <> {} and
A5: Z c= { P where P is Ideal of L : ( I c= P & P misses F ) } and
A6: Z is c=-linear ; ::_thesis: union Z in { P where P is Ideal of L : ( I c= P & P misses F ) }
Z c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in bool the carrier of L )
assume x in Z ; ::_thesis: x in bool the carrier of L
then x in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5;
then ex P being Ideal of L st
( x = P & I c= P & P misses F ) ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider ZI = Z as Subset-Family of L ;
now__::_thesis:_for_A_being_Subset_of_L_st_A_in_ZI_holds_
A_is_lower
let A be Subset of L; ::_thesis: ( A in ZI implies A is lower )
assume A in ZI ; ::_thesis: A is lower
then A in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5;
then ex P being Ideal of L st
( A = P & I c= P & P misses F ) ;
hence A is lower ; ::_thesis: verum
end;
then reconsider J = union ZI as lower Subset of L by WAYBEL_0:26;
A7: now__::_thesis:_(_I_c=_J_&_not_J_is_empty_&_(_for_A,_B_being_Subset_of_L_st_A_in_ZI_&_B_in_ZI_holds_
ex_C_being_Subset_of_L_st_
(_C_in_ZI_&_A_\/_B_c=_C_)_)_)
set y = the Element of Z;
the Element of Z in Z by A4;
then A8: I c= the Element of Z by A2, A5;
A9: the Element of Z c= J by A4, ZFMISC_1:74;
hence I c= J by A8, XBOOLE_1:1; ::_thesis: ( not J is empty & ( for A, B being Subset of L st A in ZI & B in ZI holds
ex C being Subset of L st
( C in ZI & A \/ B c= C ) ) )
thus not J is empty by A8, A9; ::_thesis: for A, B being Subset of L st A in ZI & B in ZI holds
ex C being Subset of L st
( C in ZI & A \/ B c= C )
let A, B be Subset of L; ::_thesis: ( A in ZI & B in ZI implies ex C being Subset of L st
( C in ZI & A \/ B c= C ) )
assume A10: ( A in ZI & B in ZI ) ; ::_thesis: ex C being Subset of L st
( C in ZI & A \/ B c= C )
then A,B are_c=-comparable by A6, ORDINAL1:def_8;
then ( A c= B or B c= A ) by XBOOLE_0:def_9;
then ( A \/ B = A or A \/ B = B ) by XBOOLE_1:12;
hence ex C being Subset of L st
( C in ZI & A \/ B c= C ) by A10; ::_thesis: verum
end;
now__::_thesis:_for_A_being_Subset_of_L_st_A_in_ZI_holds_
A_is_directed
let A be Subset of L; ::_thesis: ( A in ZI implies A is directed )
assume A in ZI ; ::_thesis: A is directed
then A in { P where P is Ideal of L : ( I c= P & P misses F ) } by A5;
then ex P being Ideal of L st
( A = P & I c= P & P misses F ) ;
hence A is directed ; ::_thesis: verum
end;
then reconsider J = J as Ideal of L by A7, WAYBEL_0:46;
now__::_thesis:_for_x_being_set_st_x_in_J_holds_
not_x_in_F
let x be set ; ::_thesis: ( x in J implies not x in F )
assume x in J ; ::_thesis: not x in F
then consider A being set such that
A11: x in A and
A12: A in Z by TARSKI:def_4;
A misses F by A2, A5, A12;
hence not x in F by A11, XBOOLE_0:3; ::_thesis: verum
end;
then J misses F by XBOOLE_0:3;
hence union Z in { P where P is Ideal of L : ( I c= P & P misses F ) } by A7; ::_thesis: verum
end;
I in { P where P is Ideal of L : ( I c= P & P misses F ) } by A1;
then consider Y being set such that
A13: Y in { P where P is Ideal of L : ( I c= P & P misses F ) } and
A14: for Z being set st Z in { P where P is Ideal of L : ( I c= P & P misses F ) } & Z <> Y holds
not Y c= Z by A3, ORDERS_1:67;
consider P being Ideal of L such that
A15: P = Y and
A16: I c= P and
A17: P misses F by A13;
take P ; ::_thesis: ( P is prime & I c= P & P misses F )
hereby :: according to WAYBEL_7:def_1 ::_thesis: ( I c= P & P misses F )
let x, y be Element of L; ::_thesis: ( x "/\" y in P & not x in P implies y in P )
assume that
A18: x "/\" y in P and
A19: not x in P and
A20: not y in P ; ::_thesis: contradiction
set Py = downarrow (finsups (P \/ {y}));
A21: P \/ {y} c= downarrow (finsups (P \/ {y})) by WAYBEL_0:61;
A22: P c= P \/ {y} by XBOOLE_1:7;
then P c= downarrow (finsups (P \/ {y})) by A21, XBOOLE_1:1;
then A23: I c= downarrow (finsups (P \/ {y})) by A16, XBOOLE_1:1;
y in {y} by TARSKI:def_1;
then y in P \/ {y} by XBOOLE_0:def_3;
then A24: y in downarrow (finsups (P \/ {y})) by A21;
now__::_thesis:_not_downarrow_(finsups_(P_\/_{y}))_misses_F
assume downarrow (finsups (P \/ {y})) misses F ; ::_thesis: contradiction
then downarrow (finsups (P \/ {y})) in { P where P is Ideal of L : ( I c= P & P misses F ) } by A23;
hence contradiction by A14, A15, A20, A21, A22, A24, XBOOLE_1:1; ::_thesis: verum
end;
then consider v being set such that
A25: v in downarrow (finsups (P \/ {y})) and
A26: v in F by XBOOLE_0:3;
set Px = downarrow (finsups (P \/ {x}));
A27: P \/ {x} c= downarrow (finsups (P \/ {x})) by WAYBEL_0:61;
A28: P c= P \/ {x} by XBOOLE_1:7;
then P c= downarrow (finsups (P \/ {x})) by A27, XBOOLE_1:1;
then A29: I c= downarrow (finsups (P \/ {x})) by A16, XBOOLE_1:1;
x in {x} by TARSKI:def_1;
then x in P \/ {x} by XBOOLE_0:def_3;
then A30: x in downarrow (finsups (P \/ {x})) by A27;
now__::_thesis:_not_downarrow_(finsups_(P_\/_{x}))_misses_F
assume downarrow (finsups (P \/ {x})) misses F ; ::_thesis: contradiction
then downarrow (finsups (P \/ {x})) in { P where P is Ideal of L : ( I c= P & P misses F ) } by A29;
hence contradiction by A14, A15, A19, A27, A28, A30, XBOOLE_1:1; ::_thesis: verum
end;
then consider u being set such that
A31: u in downarrow (finsups (P \/ {x})) and
A32: u in F by XBOOLE_0:3;
reconsider u = u, v = v as Element of L by A31, A25;
consider u9 being Element of L such that
A33: u9 in P and
A34: u <= u9 "\/" (sup {x}) by A31, Lm2;
consider v9 being Element of L such that
A35: v9 in P and
A36: v <= v9 "\/" (sup {y}) by A25, Lm2;
set w = u9 "\/" v9;
(v9 "\/" u9) "\/" x = v9 "\/" (u9 "\/" x) by LATTICE3:14;
then ( sup {x} = x & (u9 "\/" v9) "\/" x >= u9 "\/" x ) by YELLOW_0:22, YELLOW_0:39;
then (u9 "\/" v9) "\/" x >= u by A34, ORDERS_2:3;
then A37: (u9 "\/" v9) "\/" x in F by A32, WAYBEL_0:def_20;
(u9 "\/" v9) "\/" y = u9 "\/" (v9 "\/" y) by LATTICE3:14;
then ( sup {y} = y & (u9 "\/" v9) "\/" y >= v9 "\/" y ) by YELLOW_0:22, YELLOW_0:39;
then (u9 "\/" v9) "\/" y >= v by A36, ORDERS_2:3;
then (u9 "\/" v9) "\/" y in F by A26, WAYBEL_0:def_20;
then ((u9 "\/" v9) "\/" x) "/\" ((u9 "\/" v9) "\/" y) in F by A37, WAYBEL_0:41;
then A38: (u9 "\/" v9) "\/" (x "/\" y) in F by WAYBEL_1:5;
u9 "\/" v9 in P by A33, A35, WAYBEL_0:40;
then (u9 "\/" v9) "\/" (x "/\" y) in P by A18, WAYBEL_0:40;
hence contradiction by A17, A38, XBOOLE_0:3; ::_thesis: verum
end;
thus ( I c= P & P misses F ) by A16, A17; ::_thesis: verum
end;
theorem Th24: :: WAYBEL_7:24
for L being distributive LATTICE
for I being Ideal of L
for x being Element of L st not x in I holds
ex P being Ideal of L st
( P is prime & I c= P & not x in P )
proof
let L be distributive LATTICE; ::_thesis: for I being Ideal of L
for x being Element of L st not x in I holds
ex P being Ideal of L st
( P is prime & I c= P & not x in P )
let I be Ideal of L; ::_thesis: for x being Element of L st not x in I holds
ex P being Ideal of L st
( P is prime & I c= P & not x in P )
let x be Element of L; ::_thesis: ( not x in I implies ex P being Ideal of L st
( P is prime & I c= P & not x in P ) )
assume A1: not x in I ; ::_thesis: ex P being Ideal of L st
( P is prime & I c= P & not x in P )
now__::_thesis:_for_a_being_set_st_a_in_I_holds_
not_a_in_uparrow_x
let a be set ; ::_thesis: ( a in I implies not a in uparrow x )
assume that
A2: a in I and
A3: a in uparrow x ; ::_thesis: contradiction
reconsider a = a as Element of L by A2;
a >= x by A3, WAYBEL_0:18;
hence contradiction by A1, A2, WAYBEL_0:def_19; ::_thesis: verum
end;
then I misses uparrow x by XBOOLE_0:3;
then consider P being Ideal of L such that
A4: ( P is prime & I c= P ) and
A5: P misses uparrow x by Th23;
take P ; ::_thesis: ( P is prime & I c= P & not x in P )
thus ( P is prime & I c= P ) by A4; ::_thesis: not x in P
assume x in P ; ::_thesis: contradiction
then not x in uparrow x by A5, XBOOLE_0:3;
then not x <= x by WAYBEL_0:18;
hence contradiction ; ::_thesis: verum
end;
theorem Th25: :: WAYBEL_7:25
for L being distributive LATTICE
for I being Ideal of L
for F being Filter of L st I misses F holds
ex P being Filter of L st
( P is prime & F c= P & I misses P )
proof
let L be distributive LATTICE; ::_thesis: for I being Ideal of L
for F being Filter of L st I misses F holds
ex P being Filter of L st
( P is prime & F c= P & I misses P )
let I be Ideal of L; ::_thesis: for F being Filter of L st I misses F holds
ex P being Filter of L st
( P is prime & F c= P & I misses P )
let F be Filter of L; ::_thesis: ( I misses F implies ex P being Filter of L st
( P is prime & F c= P & I misses P ) )
assume A1: I misses F ; ::_thesis: ex P being Filter of L st
( P is prime & F c= P & I misses P )
reconsider I9 = F as Ideal of (L opp) by YELLOW_7:27, YELLOW_7:29;
reconsider F9 = I as Filter of (L opp) by YELLOW_7:26, YELLOW_7:28;
consider P9 being Ideal of (L opp) such that
A2: ( P9 is prime & I9 c= P9 & P9 misses F9 ) by A1, Th23;
reconsider P = P9 as Filter of L by YELLOW_7:27, YELLOW_7:29;
take P ; ::_thesis: ( P is prime & F c= P & I misses P )
thus ( P is prime & F c= P & I misses P ) by A2, Th17; ::_thesis: verum
end;
theorem Th26: :: WAYBEL_7:26
for L being non trivial Boolean LATTICE
for F being proper Filter of L ex G being Filter of L st
( F c= G & G is ultra )
proof
let L be non trivial Boolean LATTICE; ::_thesis: for F being proper Filter of L ex G being Filter of L st
( F c= G & G is ultra )
let F be proper Filter of L; ::_thesis: ex G being Filter of L st
( F c= G & G is ultra )
downarrow (Bottom L) = {(Bottom L)} by WAYBEL_4:23;
then reconsider I = {(Bottom L)} as Ideal of L ;
now__::_thesis:_for_a_being_set_st_a_in_I_holds_
not_a_in_F
let a be set ; ::_thesis: ( a in I implies not a in F )
assume a in I ; ::_thesis: not a in F
then a = Bottom L by TARSKI:def_1;
hence not a in F by Th4; ::_thesis: verum
end;
then I misses F by XBOOLE_0:3;
then consider G being Filter of L such that
A1: ( G is prime & F c= G ) and
A2: I misses G by Th25;
take G ; ::_thesis: ( F c= G & G is ultra )
now__::_thesis:_not_Bottom_L_in_G
assume Bottom L in G ; ::_thesis: contradiction
then not Bottom L in I by A2, XBOOLE_0:3;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
then G is proper by Th4;
hence ( F c= G & G is ultra ) by A1, Th22; ::_thesis: verum
end;
begin
definition
let T be TopSpace;
let F, x be set ;
predx is_a_cluster_point_of F,T means :Def4: :: WAYBEL_7:def 4
for A being Subset of T st A is open & x in A holds
for B being set st B in F holds
A meets B;
predx is_a_convergence_point_of F,T means :Def5: :: WAYBEL_7:def 5
for A being Subset of T st A is open & x in A holds
A in F;
end;
:: deftheorem Def4 defines is_a_cluster_point_of WAYBEL_7:def_4_:_
for T being TopSpace
for F, x being set holds
( x is_a_cluster_point_of F,T iff for A being Subset of T st A is open & x in A holds
for B being set st B in F holds
A meets B );
:: deftheorem Def5 defines is_a_convergence_point_of WAYBEL_7:def_5_:_
for T being TopSpace
for F, x being set holds
( x is_a_convergence_point_of F,T iff for A being Subset of T st A is open & x in A holds
A in F );
registration
let X be non empty set ;
cluster non empty filtered upper ultra for Element of bool the carrier of (BoolePoset X);
existence
ex b1 being Filter of (BoolePoset X) st b1 is ultra
proof
set F = the proper Filter of (BoolePoset X);
ex G being Filter of (BoolePoset X) st
( the proper Filter of (BoolePoset X) c= G & G is ultra ) by Th26;
hence ex b1 being Filter of (BoolePoset X) st b1 is ultra ; ::_thesis: verum
end;
end;
theorem Th27: :: WAYBEL_7:27
for T being non empty TopSpace
for F being ultra Filter of (BoolePoset the carrier of T)
for p being set holds
( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )
proof
let T be non empty TopSpace; ::_thesis: for F being ultra Filter of (BoolePoset the carrier of T)
for p being set holds
( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )
set L = BoolePoset the carrier of T;
let F be ultra Filter of (BoolePoset the carrier of T); ::_thesis: for p being set holds
( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )
let p be set ; ::_thesis: ( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )
thus ( p is_a_cluster_point_of F,T implies p is_a_convergence_point_of F,T ) ::_thesis: ( p is_a_convergence_point_of F,T implies p is_a_cluster_point_of F,T )
proof
assume A1: for A being Subset of T st A is open & p in A holds
for B being set st B in F holds
A meets B ; :: according to WAYBEL_7:def_4 ::_thesis: p is_a_convergence_point_of F,T
let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( A is open & p in A implies A in F )
assume that
A2: ( A is open & p in A ) and
A3: not A in F ; ::_thesis: contradiction
F is prime by Th22;
then the carrier of T \ A in F by A3, Th21;
then A meets the carrier of T \ A by A1, A2;
hence contradiction by XBOOLE_1:79; ::_thesis: verum
end;
assume A4: for A being Subset of T st A is open & p in A holds
A in F ; :: according to WAYBEL_7:def_5 ::_thesis: p is_a_cluster_point_of F,T
let A be Subset of T; :: according to WAYBEL_7:def_4 ::_thesis: ( A is open & p in A implies for B being set st B in F holds
A meets B )
assume ( A is open & p in A ) ; ::_thesis: for B being set st B in F holds
A meets B
then A5: A in F by A4;
Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
then A6: not {} in F by Th4;
let B be set ; ::_thesis: ( B in F implies A meets B )
assume A7: B in F ; ::_thesis: A meets B
then reconsider a = A, b = B as Element of (BoolePoset the carrier of T) by A5;
a "/\" b = A /\ B by YELLOW_1:17;
then A /\ B in F by A5, A7, WAYBEL_0:41;
hence A meets B by A6, XBOOLE_0:def_7; ::_thesis: verum
end;
theorem Th28: :: WAYBEL_7:28
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st x << y holds
for F being proper Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T )
proof
defpred S1[ set , set ] means $1 misses $2;
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds
for F being proper Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T )
set L = InclPoset the topology of T;
set B = BoolePoset the carrier of T;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x << y implies for F being proper Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T ) )
assume A1: x << y ; ::_thesis: for F being proper Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T )
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A2: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1;
( x in the carrier of (InclPoset the topology of T) & InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) ) by YELLOW_1:def_1;
then reconsider x9 = x as Element of (BoolePoset the carrier of T) by A2;
let F be proper Filter of (BoolePoset the carrier of T); ::_thesis: ( x in F implies ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T ) )
assume that
A3: x in F and
A4: for x being Element of T st x in y holds
not x is_a_cluster_point_of F,T ; ::_thesis: contradiction
set V = { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } ;
{ A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } or a in bool the carrier of T )
assume a in { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } ; ::_thesis: a in bool the carrier of T
then ex C being Subset of T st
( a = C & C is open & C meets y & ex B being set st
( B in F & C misses B ) ) ;
hence a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider V = { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } as Subset-Family of T ;
reconsider V = V as Subset-Family of T ;
A5: y c= union V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in y or x in union V )
assume A6: x in y ; ::_thesis: x in union V
InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
then y in the topology of T ;
then not x is_a_cluster_point_of F,T by A4, A6;
then consider A being Subset of T such that
A7: A is open and
A8: x in A and
A9: ex B being set st
( B in F & A misses B ) by Def4;
A meets y by A6, A8, XBOOLE_0:3;
then A in V by A7, A9;
hence x in union V by A8, TARSKI:def_4; ::_thesis: verum
end;
V is open
proof
let a be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not a in V or a is open )
assume a in V ; ::_thesis: a is open
then ex C being Subset of T st
( a = C & C is open & C meets y & ex B being set st
( B in F & C misses B ) ) ;
hence a is open ; ::_thesis: verum
end;
then consider W being finite Subset of V such that
A10: x c= union W by A1, A5, WAYBEL_3:34;
A11: now__::_thesis:_for_A_being_set_st_A_in_W_holds_
ex_B_being_set_st_
(_B_in_F_&_S1[A,B]_)
let A be set ; ::_thesis: ( A in W implies ex B being set st
( B in F & S1[A,B] ) )
assume A in W ; ::_thesis: ex B being set st
( B in F & S1[A,B] )
then A in V ;
then ex C being Subset of T st
( A = C & C is open & C meets y & ex B being set st
( B in F & C misses B ) ) ;
hence ex B being set st
( B in F & S1[A,B] ) ; ::_thesis: verum
end;
consider f being Function such that
A12: ( dom f = W & rng f c= F & ( for A being set st A in W holds
S1[A,f . A] ) ) from FUNCT_1:sch_5(A11);
rng f is finite by A12, FINSET_1:8;
then consider z being Element of (BoolePoset the carrier of T) such that
A13: z in F and
A14: z is_<=_than rng f by A12, WAYBEL_0:2;
set a = the Element of x9 "/\" z;
x9 "/\" z in F by A3, A13, WAYBEL_0:41;
then x9 "/\" z <> Bottom (BoolePoset the carrier of T) by Th4;
then x9 "/\" z <> {} by YELLOW_1:18;
then A15: the Element of x9 "/\" z in x9 "/\" z ;
A16: x9 "/\" z c= x9 /\ z by YELLOW_1:17;
then the Element of x9 "/\" z in x by A15, XBOOLE_0:def_4;
then consider A being set such that
A17: the Element of x9 "/\" z in A and
A18: A in W by A10, TARSKI:def_4;
A19: the Element of x9 "/\" z in z by A15, A16, XBOOLE_0:def_4;
A20: f . A in rng f by A12, A18, FUNCT_1:def_3;
then f . A in F by A12;
then reconsider b = f . A as Element of (BoolePoset the carrier of T) ;
z <= b by A14, A20, LATTICE3:def_8;
then A21: z c= b by YELLOW_1:2;
A misses b by A12, A18;
hence contradiction by A19, A17, A21, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: WAYBEL_7:29
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st x << y holds
for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
proof
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds
for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x << y implies for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) )
assume A1: x << y ; ::_thesis: for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
let F be ultra Filter of (BoolePoset the carrier of T); ::_thesis: ( x in F implies ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) )
assume x in F ; ::_thesis: ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
then consider p being Element of T such that
A2: ( p in y & p is_a_cluster_point_of F,T ) by A1, Th28;
take p ; ::_thesis: ( p in y & p is_a_convergence_point_of F,T )
thus ( p in y & p is_a_convergence_point_of F,T ) by A2, Th27; ::_thesis: verum
end;
theorem Th30: :: WAYBEL_7:30
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) ) holds
x << y
proof
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) ) holds
x << y
set B = BoolePoset the carrier of T;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x c= y & ( for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) ) implies x << y )
assume that
A1: x c= y and
A2: for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) ; ::_thesis: x << y
InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
then x in the topology of T ;
then reconsider X = x as Subset of T ;
reconsider X = X as Subset of T ;
assume not x << y ; ::_thesis: contradiction
then consider F being Subset-Family of T such that
A3: F is open and
A4: y c= union F and
A5: for G being finite Subset of F holds not x c= union G by WAYBEL_3:35;
set xF = { (x \ z) where z is Subset of T : z in F } ;
set z = the Element of F;
A6: now__::_thesis:_not_F_=_{}
assume A7: F = {} ; ::_thesis: contradiction
then A8: y = {} by A4, ZFMISC_1:2;
then x = y by A1;
hence contradiction by A1, A4, A5, A7, A8; ::_thesis: verum
end;
then A9: the Element of F in F ;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A10: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1;
{ (x \ z) where z is Subset of T : z in F } c= the carrier of (BoolePoset the carrier of T)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x \ z) where z is Subset of T : z in F } or a in the carrier of (BoolePoset the carrier of T) )
assume a in { (x \ z) where z is Subset of T : z in F } ; ::_thesis: a in the carrier of (BoolePoset the carrier of T)
then ex z being Subset of T st
( a = x \ z & z in F ) ;
then a c= X ;
then a c= the carrier of T by XBOOLE_1:1;
hence a in the carrier of (BoolePoset the carrier of T) by A10; ::_thesis: verum
end;
then reconsider xF = { (x \ z) where z is Subset of T : z in F } as Subset of (BoolePoset the carrier of T) ;
set FF = uparrow (fininfs xF);
now__::_thesis:_not_Bottom_(BoolePoset_the_carrier_of_T)_in_uparrow_(fininfs_xF)
defpred S1[ set , set ] means $1 = x \ $2;
assume Bottom (BoolePoset the carrier of T) in uparrow (fininfs xF) ; ::_thesis: contradiction
then consider a being Element of (BoolePoset the carrier of T) such that
A11: a <= Bottom (BoolePoset the carrier of T) and
A12: a in fininfs xF by WAYBEL_0:def_16;
consider s being finite Subset of xF such that
A13: a = "/\" (s,(BoolePoset the carrier of T)) and
ex_inf_of s, BoolePoset the carrier of T by A12;
reconsider t = s as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;
A14: now__::_thesis:_for_v_being_set_st_v_in_s_holds_
ex_z_being_set_st_
(_z_in_F_&_S1[v,z]_)
let v be set ; ::_thesis: ( v in s implies ex z being set st
( z in F & S1[v,z] ) )
assume v in s ; ::_thesis: ex z being set st
( z in F & S1[v,z] )
then v in xF ;
then ex z being Subset of T st
( v = x \ z & z in F ) ;
hence ex z being set st
( z in F & S1[v,z] ) ; ::_thesis: verum
end;
consider f being Function such that
A15: ( dom f = s & rng f c= F & ( for v being set st v in s holds
S1[v,f . v] ) ) from FUNCT_1:sch_5(A14);
reconsider G = rng f as finite Subset of F by A15, FINSET_1:8;
Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
then A16: a c= {} by A11, YELLOW_1:2;
A17: now__::_thesis:_not_s_=_{}
assume s = {} ; ::_thesis: contradiction
then a = Top (BoolePoset the carrier of T) by A13;
hence contradiction by A16, YELLOW_1:19; ::_thesis: verum
end;
then A18: a = meet t by A13, YELLOW_1:20;
x c= union G
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in x or c in union G )
assume that
A19: c in x and
A20: not c in union G ; ::_thesis: contradiction
now__::_thesis:_for_v_being_set_st_v_in_s_holds_
c_in_v
let v be set ; ::_thesis: ( v in s implies c in v )
assume A21: v in s ; ::_thesis: c in v
then f . v in rng f by A15, FUNCT_1:def_3;
then A22: not c in f . v by A20, TARSKI:def_4;
v = x \ (f . v) by A15, A21;
hence c in v by A19, A22, XBOOLE_0:def_5; ::_thesis: verum
end;
hence contradiction by A16, A17, A18, SETFAM_1:def_1; ::_thesis: verum
end;
hence contradiction by A5; ::_thesis: verum
end;
then uparrow (fininfs xF) is proper by Th4;
then consider GG being Filter of (BoolePoset the carrier of T) such that
A23: uparrow (fininfs xF) c= GG and
A24: GG is ultra by Th26;
reconsider z = the Element of F as Subset of T by A9;
A25: xF c= uparrow (fininfs xF) by WAYBEL_0:62;
x \ z in xF by A6;
then A26: x \ z in uparrow (fininfs xF) by A25;
x \ z c= X ;
then x in GG by A23, A26, Th7;
then consider p being Element of T such that
A27: p in y and
A28: p is_a_convergence_point_of GG,T by A2, A24;
consider W being set such that
A29: p in W and
A30: W in F by A4, A27, TARSKI:def_4;
reconsider W = W as Subset of T by A30;
W is open by A3, A30, TOPS_2:def_1;
then A31: W in GG by A28, A29, Def5;
A32: xF c= uparrow (fininfs xF) by WAYBEL_0:62;
x \ W in xF by A30;
then x \ W in uparrow (fininfs xF) by A32;
then ( W misses x \ W & W /\ (x \ W) in GG ) by A23, A31, Th9, XBOOLE_1:79;
then {} in GG by XBOOLE_0:def_7;
then Bottom (BoolePoset the carrier of T) in GG by YELLOW_1:18;
hence contradiction by A24, Th4; ::_thesis: verum
end;
theorem :: WAYBEL_7:31
for T being non empty TopSpace
for B being prebasis of T
for x, y being Element of (InclPoset the topology of T) st x c= y holds
( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
proof
let T be non empty TopSpace; ::_thesis: for B being prebasis of T
for x, y being Element of (InclPoset the topology of T) st x c= y holds
( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
let B be prebasis of T; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x c= y holds
( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
consider BB being Basis of T such that
A1: BB c= FinMeetCl B by CANTOR_1:def_4;
set BT = BoolePoset the carrier of T;
set L = InclPoset the topology of T;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x c= y implies ( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ) )
assume A2: x c= y ; ::_thesis: ( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
A3: B c= the topology of T by TOPS_2:64;
hereby ::_thesis: ( ( for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ) implies x << y )
assume A4: x << y ; ::_thesis: for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G
let F be Subset of B; ::_thesis: ( y c= union F implies ex G being finite Subset of F st x c= union G )
assume A5: y c= union F ; ::_thesis: ex G being finite Subset of F st x c= union G
reconsider FF = F as Subset-Family of T by XBOOLE_1:1;
FF is open
proof
let a be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not a in FF or a is open )
assume a in FF ; ::_thesis: a is open
then a in B ;
hence a in the topology of T by A3; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
hence ex G being finite Subset of F st x c= union G by A4, A5, WAYBEL_3:34; ::_thesis: verum
end;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A6: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1;
InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
then ( x in the topology of T & y in the topology of T ) ;
then reconsider X = x, Y = y as Subset of T ;
assume A7: for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ; ::_thesis: x << y
A8: the topology of T c= UniCl BB by CANTOR_1:def_2;
now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_the_carrier_of_T)_st_x_in_F_holds_
ex_p_being_Element_of_T_st_
(_p_in_y_&_p_is_a_convergence_point_of_F,T_)
deffunc H1( set ) -> Element of bool x = x \ $1;
let F be ultra Filter of (BoolePoset the carrier of T); ::_thesis: ( x in F implies ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) )
assume that
A9: x in F and
A10: for p being Element of T holds
( not p in y or not p is_a_convergence_point_of F,T ) ; ::_thesis: contradiction
defpred S1[ set , set ] means ( $1 in $2 & not $2 in F );
A11: now__::_thesis:_for_p_being_set_st_p_in_y_holds_
ex_r_being_set_st_
(_r_in_B_&_S1[p,r]_)
let p be set ; ::_thesis: ( p in y implies ex r being set st
( r in B & S1[p,r] ) )
assume A12: p in y ; ::_thesis: ex r being set st
( r in B & S1[p,r] )
then p in Y ;
then reconsider q = p as Element of T ;
not q is_a_convergence_point_of F,T by A10, A12;
then consider A being Subset of T such that
A13: A is open and
A14: q in A and
A15: not A in F by Def5;
A in the topology of T by A13, PRE_TOPC:def_2;
then consider AY being Subset-Family of T such that
A16: AY c= BB and
A17: A = union AY by A8, CANTOR_1:def_1;
consider ay being set such that
A18: q in ay and
A19: ay in AY by A14, A17, TARSKI:def_4;
reconsider ay = ay as Subset of T by A19;
ay in BB by A16, A19;
then consider BY being Subset-Family of T such that
A20: BY c= B and
A21: BY is finite and
A22: ay = Intersect BY by A1, CANTOR_1:def_3;
ay c= A by A17, A19, ZFMISC_1:74;
then not ay in F by A15, Th7;
then BY is not Subset of F by A21, A22, Th11;
then consider r being set such that
A23: ( r in BY & not r in F ) by TARSKI:def_3;
take r = r; ::_thesis: ( r in B & S1[p,r] )
thus ( r in B & S1[p,r] ) by A18, A20, A22, A23, SETFAM_1:43; ::_thesis: verum
end;
consider f being Function such that
A24: ( dom f = y & rng f c= B ) and
A25: for p being set st p in y holds
S1[p,f . p] from FUNCT_1:sch_5(A11);
reconsider FF = rng f as Subset of B by A24;
y c= union FF
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in y or p in union FF )
assume p in y ; ::_thesis: p in union FF
then ( f . p in FF & p in f . p ) by A24, A25, FUNCT_1:def_3;
hence p in union FF by TARSKI:def_4; ::_thesis: verum
end;
then consider G being finite Subset of FF such that
A26: x c= union G by A7;
set gg = the Element of G;
consider g being Function such that
A27: ( dom g = G & ( for z being set st z in G holds
g . z = H1(z) ) ) from FUNCT_1:sch_3();
A28: rng g c= F
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g or a in F )
A29: F is prime by Th22;
assume a in rng g ; ::_thesis: a in F
then consider b being set such that
A30: b in G and
A31: a = g . b by A27, FUNCT_1:def_3;
b in FF by A30;
then b in B ;
then reconsider b = b as Subset of T ;
ex p being set st
( p in y & b = f . p ) by A24, A30, FUNCT_1:def_3;
then not b in F by A25;
then A32: the carrier of T \ b in F by A29, Th21;
a = x \ b by A27, A30, A31
.= X /\ (b `) by SUBSET_1:13
.= x /\ ( the carrier of T \ b) ;
hence a in F by A9, A32, Th9; ::_thesis: verum
end;
then reconsider GG = rng g as finite Subset-Family of T by A6, A27, FINSET_1:8, XBOOLE_1:1;
x <> Bottom (BoolePoset the carrier of T) by A9, Th4;
then x <> {} by YELLOW_1:18;
then A33: G <> {} by A26, ZFMISC_1:2;
now__::_thesis:_for_a_being_set_holds_not_a_in_Intersect_GG
let a be set ; ::_thesis: not a in Intersect GG
assume A34: a in Intersect GG ; ::_thesis: contradiction
now__::_thesis:_for_z_being_set_st_z_in_G_holds_
not_a_in_z
let z be set ; ::_thesis: ( z in G implies not a in z )
assume z in G ; ::_thesis: not a in z
then ( g . z in GG & g . z = x \ z ) by A27, FUNCT_1:def_3;
then a in x \ z by A34, SETFAM_1:43;
hence not a in z by XBOOLE_0:def_5; ::_thesis: verum
end;
then for z being set holds
( not a in z or not z in G ) ;
then A35: not a in x by A26, TARSKI:def_4;
( g . the Element of G in GG & g . the Element of G = x \ the Element of G ) by A33, A27, FUNCT_1:def_3;
then a in x \ the Element of G by A34, SETFAM_1:43;
hence contradiction by A35; ::_thesis: verum
end;
then A36: Intersect GG = {} by XBOOLE_0:def_1;
Intersect GG in F by A28, Th11;
then Bottom (BoolePoset the carrier of T) in F by A36, YELLOW_1:18;
hence contradiction by Th4; ::_thesis: verum
end;
hence x << y by A2, Th30; ::_thesis: verum
end;
theorem :: WAYBEL_7:32
for L being distributive complete LATTICE
for x, y being Element of L holds
( x << y iff for P being prime Ideal of L st y <= sup P holds
x in P )
proof
let L be distributive complete LATTICE; ::_thesis: for x, y being Element of L holds
( x << y iff for P being prime Ideal of L st y <= sup P holds
x in P )
let x, y be Element of L; ::_thesis: ( x << y iff for P being prime Ideal of L st y <= sup P holds
x in P )
thus ( x << y implies for P being prime Ideal of L st y <= sup P holds
x in P ) by WAYBEL_3:20; ::_thesis: ( ( for P being prime Ideal of L st y <= sup P holds
x in P ) implies x << y )
assume A1: for P being prime Ideal of L st y <= sup P holds
x in P ; ::_thesis: x << y
now__::_thesis:_for_I_being_Ideal_of_L_st_y_<=_sup_I_holds_
x_in_I
let I be Ideal of L; ::_thesis: ( y <= sup I implies x in I )
assume that
A2: y <= sup I and
A3: not x in I ; ::_thesis: contradiction
consider P being Ideal of L such that
A4: P is prime and
A5: I c= P and
A6: not x in P by A3, Th24;
sup I <= sup P by A5, Th1;
hence contradiction by A1, A2, A4, A6, ORDERS_2:3; ::_thesis: verum
end;
hence x << y by WAYBEL_3:21; ::_thesis: verum
end;
theorem Th33: :: WAYBEL_7:33
for L being LATTICE
for p being Element of L st p is prime holds
downarrow p is prime
proof
let L be LATTICE; ::_thesis: for p being Element of L st p is prime holds
downarrow p is prime
let p be Element of L; ::_thesis: ( p is prime implies downarrow p is prime )
assume A1: for x, y being Element of L holds
( not x "/\" y <= p or x <= p or y <= p ) ; :: according to WAYBEL_6:def_6 ::_thesis: downarrow p is prime
let x, y be Element of L; :: according to WAYBEL_7:def_1 ::_thesis: ( not x "/\" y in downarrow p or x in downarrow p or y in downarrow p )
assume x "/\" y in downarrow p ; ::_thesis: ( x in downarrow p or y in downarrow p )
then x "/\" y <= p by WAYBEL_0:17;
then ( x <= p or y <= p ) by A1;
hence ( x in downarrow p or y in downarrow p ) by WAYBEL_0:17; ::_thesis: verum
end;
begin
definition
let L be LATTICE;
let p be Element of L;
attrp is pseudoprime means :Def6: :: WAYBEL_7:def 6
ex P being prime Ideal of L st p = sup P;
end;
:: deftheorem Def6 defines pseudoprime WAYBEL_7:def_6_:_
for L being LATTICE
for p being Element of L holds
( p is pseudoprime iff ex P being prime Ideal of L st p = sup P );
theorem Th34: :: WAYBEL_7:34
for L being LATTICE
for p being Element of L st p is prime holds
p is pseudoprime
proof
let L be LATTICE; ::_thesis: for p being Element of L st p is prime holds
p is pseudoprime
let p be Element of L; ::_thesis: ( p is prime implies p is pseudoprime )
assume p is prime ; ::_thesis: p is pseudoprime
then A1: downarrow p is prime by Th33;
p = sup (downarrow p) by WAYBEL_0:34;
hence ex P being prime Ideal of L st p = sup P by A1; :: according to WAYBEL_7:def_6 ::_thesis: verum
end;
theorem Th35: :: WAYBEL_7:35
for L being continuous LATTICE
for p being Element of L st p is pseudoprime holds
for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
proof
let L be continuous LATTICE; ::_thesis: for p being Element of L st p is pseudoprime holds
for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
let p be Element of L; ::_thesis: ( p is pseudoprime implies for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) )
given P being prime Ideal of L such that A1: p = sup P ; :: according to WAYBEL_7:def_6 ::_thesis: for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
let A be non empty finite Subset of L; ::_thesis: ( inf A << p implies ex a being Element of L st
( a in A & a <= p ) )
assume inf A << p ; ::_thesis: ex a being Element of L st
( a in A & a <= p )
then A2: inf A in waybelow p ;
waybelow p c= P by A1, WAYBEL_5:1;
then consider a being Element of L such that
A3: ( a in A & a in P ) by A2, Th12;
take a ; ::_thesis: ( a in A & a <= p )
ex_sup_of P,L by WAYBEL_0:75;
then P is_<=_than p by A1, YELLOW_0:30;
hence ( a in A & a <= p ) by A3, LATTICE3:def_9; ::_thesis: verum
end;
theorem :: WAYBEL_7:36
for L being continuous LATTICE
for p being Element of L st ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) ) holds
uparrow (fininfs ((downarrow p) `)) misses waybelow p
proof
let L be continuous LATTICE; ::_thesis: for p being Element of L st ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) ) holds
uparrow (fininfs ((downarrow p) `)) misses waybelow p
let p be Element of L; ::_thesis: ( ( p <> Top L or not Top L is compact ) & ( for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) ) implies uparrow (fininfs ((downarrow p) `)) misses waybelow p )
assume that
A1: ( p <> Top L or not Top L is compact ) and
A2: for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) ; ::_thesis: uparrow (fininfs ((downarrow p) `)) misses waybelow p
now__::_thesis:_for_x_being_set_st_x_in_uparrow_(fininfs_((downarrow_p)_`))_holds_
not_x_in_waybelow_p
let x be set ; ::_thesis: ( x in uparrow (fininfs ((downarrow p) `)) implies not x in waybelow p )
assume A3: x in uparrow (fininfs ((downarrow p) `)) ; ::_thesis: not x in waybelow p
then reconsider a = x as Element of L ;
consider b being Element of L such that
A4: a >= b and
A5: b in fininfs ((downarrow p) `) by A3, WAYBEL_0:def_16;
assume x in waybelow p ; ::_thesis: contradiction
then A6: a << p by WAYBEL_3:7;
then A7: b << p by A4, WAYBEL_3:2;
consider Y being finite Subset of ((downarrow p) `) such that
A8: b = "/\" (Y,L) and
ex_inf_of Y,L by A5;
reconsider Y = Y as finite Subset of L by XBOOLE_1:1;
percases ( Y <> {} or Y = {} ) ;
suppose Y <> {} ; ::_thesis: contradiction
then consider c being Element of L such that
A9: c in Y and
A10: c <= p by A2, A4, A8, A6, WAYBEL_3:2;
c in downarrow p by A10, WAYBEL_0:17;
then ( downarrow p misses (downarrow p) ` & c in (downarrow p) /\ ((downarrow p) `) ) by A9, XBOOLE_0:def_4, XBOOLE_1:79;
hence contradiction by XBOOLE_0:def_7; ::_thesis: verum
end;
supposeA11: Y = {} ; ::_thesis: contradiction
( b <= p & p <= Top L ) by A7, WAYBEL_3:1, YELLOW_0:45;
then p = Top L by A8, A11, ORDERS_2:2;
hence contradiction by A1, A8, A7, A11, WAYBEL_3:def_2; ::_thesis: verum
end;
end;
end;
hence uparrow (fininfs ((downarrow p) `)) misses waybelow p by XBOOLE_0:3; ::_thesis: verum
end;
theorem :: WAYBEL_7:37
for L being continuous LATTICE st Top L is compact holds
( ( for A being non empty finite Subset of L st inf A << Top L holds
ex a being Element of L st
( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) )
proof
let L be continuous LATTICE; ::_thesis: ( Top L is compact implies ( ( for A being non empty finite Subset of L st inf A << Top L holds
ex a being Element of L st
( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) ) )
assume A1: Top L << Top L ; :: according to WAYBEL_3:def_2 ::_thesis: ( ( for A being non empty finite Subset of L st inf A << Top L holds
ex a being Element of L st
( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) )
A2: now__::_thesis:_ex_x_being_Element_of_the_carrier_of_L_st_
(_x_in_uparrow_(fininfs_((downarrow_(Top_L))_`))_&_x_in_waybelow_(Top_L)_)
take x = Top L; ::_thesis: ( x in uparrow (fininfs ((downarrow (Top L)) `)) & x in waybelow (Top L) )
thus x in uparrow (fininfs ((downarrow (Top L)) `)) by WAYBEL_4:22; ::_thesis: x in waybelow (Top L)
thus x in waybelow (Top L) by A1; ::_thesis: verum
end;
hereby ::_thesis: uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L)
let A be non empty finite Subset of L; ::_thesis: ( inf A << Top L implies ex a being Element of L st
( a in A & a <= Top L ) )
assume inf A << Top L ; ::_thesis: ex a being Element of L st
( a in A & a <= Top L )
set a = the Element of A;
reconsider a = the Element of A as Element of L ;
take a = a; ::_thesis: ( a in A & a <= Top L )
thus ( a in A & a <= Top L ) by YELLOW_0:45; ::_thesis: verum
end;
thus uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) by A2, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: WAYBEL_7:38
for L being continuous LATTICE
for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds
for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
proof
let L be continuous LATTICE; ::_thesis: for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds
for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
let p be Element of L; ::_thesis: ( uparrow (fininfs ((downarrow p) `)) misses waybelow p implies for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) )
assume A1: uparrow (fininfs ((downarrow p) `)) misses waybelow p ; ::_thesis: for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
let A be non empty finite Subset of L; ::_thesis: ( inf A << p implies ex a being Element of L st
( a in A & a <= p ) )
assume inf A << p ; ::_thesis: ex a being Element of L st
( a in A & a <= p )
then inf A in waybelow p ;
then not inf A in uparrow (fininfs ((downarrow p) `)) by A1, XBOOLE_0:3;
then ( (downarrow p) ` c= uparrow (fininfs ((downarrow p) `)) & not A c= uparrow (fininfs ((downarrow p) `)) ) by WAYBEL_0:43, WAYBEL_0:62;
then not A c= (downarrow p) ` by XBOOLE_1:1;
then consider a being set such that
A2: a in A and
A3: not a in (downarrow p) ` by TARSKI:def_3;
reconsider a = a as Element of L by A2;
take a ; ::_thesis: ( a in A & a <= p )
a in downarrow p by A3, SUBSET_1:29;
hence ( a in A & a <= p ) by A2, WAYBEL_0:17; ::_thesis: verum
end;
theorem :: WAYBEL_7:39
for L being distributive continuous LATTICE
for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds
p is pseudoprime
proof
let L be distributive continuous LATTICE; ::_thesis: for p being Element of L st uparrow (fininfs ((downarrow p) `)) misses waybelow p holds
p is pseudoprime
let p be Element of L; ::_thesis: ( uparrow (fininfs ((downarrow p) `)) misses waybelow p implies p is pseudoprime )
set I = waybelow p;
set F = uparrow (fininfs ((downarrow p) `));
A1: ( ex_sup_of downarrow p,L & sup (downarrow p) = p ) by WAYBEL_0:34;
(downarrow p) ` c= uparrow (fininfs ((downarrow p) `)) by WAYBEL_0:62;
then A2: (uparrow (fininfs ((downarrow p) `))) ` c= ((downarrow p) `) ` by SUBSET_1:12;
assume uparrow (fininfs ((downarrow p) `)) misses waybelow p ; ::_thesis: p is pseudoprime
then consider P being Ideal of L such that
A3: P is prime and
A4: waybelow p c= P and
A5: P misses uparrow (fininfs ((downarrow p) `)) by Th23;
reconsider P = P as prime Ideal of L by A3;
A6: ex_sup_of P,L by WAYBEL_0:75;
( ex_sup_of waybelow p,L & p = sup (waybelow p) ) by WAYBEL_0:75, WAYBEL_3:def_5;
then A7: sup P >= p by A4, A6, YELLOW_0:34;
take P ; :: according to WAYBEL_7:def_6 ::_thesis: p = sup P
P c= (uparrow (fininfs ((downarrow p) `))) ` by A5, SUBSET_1:23;
then sup P <= p by A6, A2, A1, XBOOLE_1:1, YELLOW_0:34;
hence p = sup P by A7, ORDERS_2:2; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
let R be Relation of the carrier of L;
attrR is multiplicative means :Def7: :: WAYBEL_7:def 7
for a, x, y being Element of L st [a,x] in R & [a,y] in R holds
[a,(x "/\" y)] in R;
end;
:: deftheorem Def7 defines multiplicative WAYBEL_7:def_7_:_
for L being non empty RelStr
for R being Relation of the carrier of L holds
( R is multiplicative iff for a, x, y being Element of L st [a,x] in R & [a,y] in R holds
[a,(x "/\" y)] in R );
registration
let L be lower-bounded sup-Semilattice;
let R be auxiliary Relation of L;
let x be Element of L;
clusterR -above x -> upper ;
coherence
R -above x is upper
proof
let y, z be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not y in R -above x or not y <= z or z in R -above x )
assume that
A1: y in R -above x and
A2: y <= z ; ::_thesis: z in R -above x
( x <= x & [x,y] in R ) by A1, WAYBEL_4:14;
then [x,z] in R by A2, WAYBEL_4:def_4;
hence z in R -above x by WAYBEL_4:14; ::_thesis: verum
end;
end;
theorem :: WAYBEL_7:40
for L being lower-bounded LATTICE
for R being auxiliary Relation of L holds
( R is multiplicative iff for x being Element of L holds R -above x is filtered )
proof
let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds
( R is multiplicative iff for x being Element of L holds R -above x is filtered )
let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff for x being Element of L holds R -above x is filtered )
hereby ::_thesis: ( ( for x being Element of L holds R -above x is filtered ) implies R is multiplicative )
assume A1: R is multiplicative ; ::_thesis: for x being Element of L holds R -above x is filtered
let x be Element of L; ::_thesis: R -above x is filtered
thus R -above x is filtered ::_thesis: verum
proof
let y, z be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not y in R -above x or not z in R -above x or ex b1 being Element of the carrier of L st
( b1 in R -above x & b1 <= y & b1 <= z ) )
assume ( y in R -above x & z in R -above x ) ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in R -above x & b1 <= y & b1 <= z )
then ( [x,y] in R & [x,z] in R ) by WAYBEL_4:14;
then [x,(y "/\" z)] in R by A1, Def7;
then A2: y "/\" z in R -above x by WAYBEL_4:14;
( y >= y "/\" z & z >= y "/\" z ) by YELLOW_0:23;
hence ex b1 being Element of the carrier of L st
( b1 in R -above x & b1 <= y & b1 <= z ) by A2; ::_thesis: verum
end;
end;
assume A3: for x being Element of L holds R -above x is filtered ; ::_thesis: R is multiplicative
let a, x, y be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: ( [a,x] in R & [a,y] in R implies [a,(x "/\" y)] in R )
assume ( [a,x] in R & [a,y] in R ) ; ::_thesis: [a,(x "/\" y)] in R
then A4: ( x in R -above a & y in R -above a ) by WAYBEL_4:14;
R -above a is filtered by A3;
then x "/\" y in R -above a by A4, WAYBEL_0:41;
hence [a,(x "/\" y)] in R by WAYBEL_4:14; ::_thesis: verum
end;
theorem Th41: :: WAYBEL_7:41
for L being lower-bounded LATTICE
for R being auxiliary Relation of L holds
( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R )
proof
let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds
( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R )
let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R )
hereby ::_thesis: ( ( for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R ) implies R is multiplicative )
assume A1: R is multiplicative ; ::_thesis: for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R
let a, b, x, y be Element of L; ::_thesis: ( [a,x] in R & [b,y] in R implies [(a "/\" b),(x "/\" y)] in R )
assume that
A2: [a,x] in R and
A3: [b,y] in R ; ::_thesis: [(a "/\" b),(x "/\" y)] in R
( a "/\" b <= b & y <= y ) by YELLOW_0:23;
then A4: [(a "/\" b),y] in R by A3, WAYBEL_4:def_4;
( a >= a "/\" b & x <= x ) by YELLOW_0:23;
then [(a "/\" b),x] in R by A2, WAYBEL_4:def_4;
hence [(a "/\" b),(x "/\" y)] in R by A1, A4, Def7; ::_thesis: verum
end;
assume A5: for a, b, x, y being Element of L st [a,x] in R & [b,y] in R holds
[(a "/\" b),(x "/\" y)] in R ; ::_thesis: R is multiplicative
let a be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: for x, y being Element of L st [a,x] in R & [a,y] in R holds
[a,(x "/\" y)] in R
a "/\" a = a by YELLOW_0:25;
hence for x, y being Element of L st [a,x] in R & [a,y] in R holds
[a,(x "/\" y)] in R by A5; ::_thesis: verum
end;
theorem :: WAYBEL_7:42
for L being lower-bounded LATTICE
for R being auxiliary Relation of L holds
( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting )
proof
let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds
( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting )
let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting )
reconsider X = R as Subset of [:L,L:] by YELLOW_3:def_2;
A1: X = the carrier of (subrelstr X) by YELLOW_0:def_15;
hereby ::_thesis: ( ( for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting ) implies R is multiplicative )
assume A2: R is multiplicative ; ::_thesis: for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting
let S be full SubRelStr of [:L,L:]; ::_thesis: ( the carrier of S = R implies S is meet-inheriting )
assume A3: the carrier of S = R ; ::_thesis: S is meet-inheriting
thus S is meet-inheriting ::_thesis: verum
proof
let x, y be Element of [:L,L:]; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S )
assume A4: ( x in the carrier of S & y in the carrier of S ) ; ::_thesis: ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S )
the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by YELLOW_3:def_2;
then A5: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;
ex_inf_of {x,y},[:L,L:] by YELLOW_0:21;
then inf {x,y} = [(inf (proj1 {x,y})),(inf (proj2 {x,y}))] by YELLOW_3:47
.= [(inf {(x `1),(y `1)}),(inf (proj2 {x,y}))] by A5, FUNCT_5:13
.= [(inf {(x `1),(y `1)}),(inf {(x `2),(y `2)})] by A5, FUNCT_5:13
.= [((x `1) "/\" (y `1)),(inf {(x `2),(y `2)})] by YELLOW_0:40
.= [((x `1) "/\" (y `1)),((x `2) "/\" (y `2))] by YELLOW_0:40 ;
hence ( not ex_inf_of {x,y},[:L,L:] or "/\" ({x,y},[:L,L:]) in the carrier of S ) by A2, A3, A4, A5, Th41; ::_thesis: verum
end;
end;
assume for S being full SubRelStr of [:L,L:] st the carrier of S = R holds
S is meet-inheriting ; ::_thesis: R is multiplicative
then A6: subrelstr X is meet-inheriting by A1;
let a, x, y be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: ( [a,x] in R & [a,y] in R implies [a,(x "/\" y)] in R )
A7: ex_inf_of {[a,x],[a,y]},[:L,L:] by YELLOW_0:21;
assume ( [a,x] in R & [a,y] in R ) ; ::_thesis: [a,(x "/\" y)] in R
then inf {[a,x],[a,y]} in R by A1, A6, A7, YELLOW_0:def_16;
then A8: [a,x] "/\" [a,y] in R by YELLOW_0:40;
set ax = [a,x];
set ay = [a,y];
[a,x] "/\" [a,y] = inf {[a,x],[a,y]} by YELLOW_0:40
.= [(inf (proj1 {[a,x],[a,y]})),(inf (proj2 {[a,x],[a,y]}))] by A7, YELLOW_3:47
.= [(inf {a,a}),(inf (proj2 {[a,x],[a,y]}))] by FUNCT_5:13
.= [(inf {a,a}),(inf {x,y})] by FUNCT_5:13
.= [(a "/\" a),(inf {x,y})] by YELLOW_0:40
.= [(a "/\" a),(x "/\" y)] by YELLOW_0:40 ;
hence [a,(x "/\" y)] in R by A8, YELLOW_0:25; ::_thesis: verum
end;
theorem :: WAYBEL_7:43
for L being lower-bounded LATTICE
for R being auxiliary Relation of L holds
( R is multiplicative iff R -below is meet-preserving )
proof
let L be lower-bounded LATTICE; ::_thesis: for R being auxiliary Relation of L holds
( R is multiplicative iff R -below is meet-preserving )
let R be auxiliary Relation of L; ::_thesis: ( R is multiplicative iff R -below is meet-preserving )
hereby ::_thesis: ( R -below is meet-preserving implies R is multiplicative )
assume A1: R is multiplicative ; ::_thesis: R -below is meet-preserving
thus R -below is meet-preserving ::_thesis: verum
proof
let x, y be Element of L; :: according to WAYBEL_0:def_34 ::_thesis: R -below preserves_inf_of {x,y}
A2: (R -below) . y = R -below y by WAYBEL_4:def_12;
A3: R -below (x "/\" y) = (R -below x) /\ (R -below y)
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (R -below x) /\ (R -below y) c= R -below (x "/\" y)
let a be set ; ::_thesis: ( a in R -below (x "/\" y) implies a in (R -below x) /\ (R -below y) )
assume a in R -below (x "/\" y) ; ::_thesis: a in (R -below x) /\ (R -below y)
then a in { z where z is Element of L : [z,(x "/\" y)] in R } by WAYBEL_4:def_10;
then consider z being Element of L such that
A4: a = z and
A5: [z,(x "/\" y)] in R ;
A6: z <= z ;
x "/\" y <= y by YELLOW_0:23;
then [z,y] in R by A5, A6, WAYBEL_4:def_4;
then A7: z in R -below y by WAYBEL_4:13;
x "/\" y <= x by YELLOW_0:23;
then [z,x] in R by A5, A6, WAYBEL_4:def_4;
then z in R -below x by WAYBEL_4:13;
hence a in (R -below x) /\ (R -below y) by A4, A7, XBOOLE_0:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (R -below x) /\ (R -below y) or a in R -below (x "/\" y) )
assume A8: a in (R -below x) /\ (R -below y) ; ::_thesis: a in R -below (x "/\" y)
then reconsider z = a as Element of L ;
a in R -below y by A8, XBOOLE_0:def_4;
then A9: [z,y] in R by WAYBEL_4:13;
a in R -below x by A8, XBOOLE_0:def_4;
then [z,x] in R by WAYBEL_4:13;
then [z,(x "/\" y)] in R by A1, A9, Def7;
hence a in R -below (x "/\" y) by WAYBEL_4:13; ::_thesis: verum
end;
( (R -below) . (x "/\" y) = R -below (x "/\" y) & (R -below) . x = R -below x ) by WAYBEL_4:def_12;
then (R -below) . (x "/\" y) = ((R -below) . x) "/\" ((R -below) . y) by A2, A3, YELLOW_2:43;
hence R -below preserves_inf_of {x,y} by YELLOW_3:8; ::_thesis: verum
end;
end;
assume A10: for x, y being Element of L holds R -below preserves_inf_of {x,y} ; :: according to WAYBEL_0:def_34 ::_thesis: R is multiplicative
let a, x, y be Element of L; :: according to WAYBEL_7:def_7 ::_thesis: ( [a,x] in R & [a,y] in R implies [a,(x "/\" y)] in R )
R -below preserves_inf_of {x,y} by A10;
then A11: (R -below) . (x "/\" y) = ((R -below) . x) "/\" ((R -below) . y) by YELLOW_3:8
.= ((R -below) . x) /\ ((R -below) . y) by YELLOW_2:43 ;
A12: (R -below) . y = R -below y by WAYBEL_4:def_12;
assume ( [a,x] in R & [a,y] in R ) ; ::_thesis: [a,(x "/\" y)] in R
then A13: ( a in R -below x & a in R -below y ) by WAYBEL_4:13;
( (R -below) . (x "/\" y) = R -below (x "/\" y) & (R -below) . x = R -below x ) by WAYBEL_4:def_12;
then a in R -below (x "/\" y) by A11, A12, A13, XBOOLE_0:def_4;
hence [a,(x "/\" y)] in R by WAYBEL_4:13; ::_thesis: verum
end;
Lm3: now__::_thesis:_for_L_being_lower-bounded_continuous_LATTICE
for_p_being_Element_of_L_st_L_-waybelow_is_multiplicative_&_(_for_a,_b_being_Element_of_L_holds_
(_not_a_"/\"_b_<<_p_or_a_<=_p_or_b_<=_p_)_)_holds_
p_is_prime
let L be lower-bounded continuous LATTICE; ::_thesis: for p being Element of L st L -waybelow is multiplicative & ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) holds
p is prime
let p be Element of L; ::_thesis: ( L -waybelow is multiplicative & ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) implies p is prime )
assume that
A1: L -waybelow is multiplicative and
A2: for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) and
A3: not p is prime ; ::_thesis: contradiction
consider x, y being Element of L such that
A4: x "/\" y <= p and
A5: not x <= p and
A6: not y <= p by A3, WAYBEL_6:def_6;
A7: for a being Element of L holds
( not waybelow a is empty & waybelow a is directed ) ;
then consider u being Element of L such that
A8: u << x and
A9: not u <= p by A5, WAYBEL_3:24;
consider v being Element of L such that
A10: v << y and
A11: not v <= p by A6, A7, WAYBEL_3:24;
A12: [v,y] in L -waybelow by A10, WAYBEL_4:def_1;
[u,x] in L -waybelow by A8, WAYBEL_4:def_1;
then [(u "/\" v),(x "/\" y)] in L -waybelow by A1, A12, Th41;
then u "/\" v << x "/\" y by WAYBEL_4:def_1;
then u "/\" v << p by A4, WAYBEL_3:2;
hence contradiction by A2, A9, A11; ::_thesis: verum
end;
theorem Th44: :: WAYBEL_7:44
for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds
for p being Element of L holds
( p is pseudoprime iff for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: ( L -waybelow is multiplicative implies for p being Element of L holds
( p is pseudoprime iff for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) )
assume A1: L -waybelow is multiplicative ; ::_thesis: for p being Element of L holds
( p is pseudoprime iff for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) )
let p be Element of L; ::_thesis: ( p is pseudoprime iff for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) )
hereby ::_thesis: ( ( for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ) implies p is pseudoprime )
assume A2: p is pseudoprime ; ::_thesis: for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p )
let a, b be Element of L; ::_thesis: ( not a "/\" b << p or a <= p or b <= p )
assume a "/\" b << p ; ::_thesis: ( a <= p or b <= p )
then inf {a,b} << p by YELLOW_0:40;
then ex c being Element of L st
( c in {a,b} & c <= p ) by A2, Th35;
hence ( a <= p or b <= p ) by TARSKI:def_2; ::_thesis: verum
end;
assume for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) ; ::_thesis: p is pseudoprime
hence p is pseudoprime by A1, Lm3, Th34; ::_thesis: verum
end;
theorem :: WAYBEL_7:45
for L being lower-bounded continuous LATTICE st L -waybelow is multiplicative holds
for p being Element of L st p is pseudoprime holds
p is prime
proof
let L be lower-bounded continuous LATTICE; ::_thesis: ( L -waybelow is multiplicative implies for p being Element of L st p is pseudoprime holds
p is prime )
assume A1: L -waybelow is multiplicative ; ::_thesis: for p being Element of L st p is pseudoprime holds
p is prime
let p be Element of L; ::_thesis: ( p is pseudoprime implies p is prime )
assume p is pseudoprime ; ::_thesis: p is prime
then for a, b being Element of L holds
( not a "/\" b << p or a <= p or b <= p ) by A1, Th44;
hence p is prime by A1, Lm3; ::_thesis: verum
end;
theorem :: WAYBEL_7:46
for L being lower-bounded distributive continuous LATTICE st ( for p being Element of L st p is pseudoprime holds
p is prime ) holds
L -waybelow is multiplicative
proof
let L be lower-bounded distributive continuous LATTICE; ::_thesis: ( ( for p being Element of L st p is pseudoprime holds
p is prime ) implies L -waybelow is multiplicative )
assume A1: for p being Element of L st p is pseudoprime holds
p is prime ; ::_thesis: L -waybelow is multiplicative
given a, x, y being Element of L such that A2: ( [a,x] in L -waybelow & [a,y] in L -waybelow ) and
A3: not [a,(x "/\" y)] in L -waybelow ; :: according to WAYBEL_7:def_7 ::_thesis: contradiction
now__::_thesis:_for_z_being_set_st_z_in_waybelow_(x_"/\"_y)_holds_
not_z_in_uparrow_a
let z be set ; ::_thesis: ( z in waybelow (x "/\" y) implies not z in uparrow a )
assume that
A4: z in waybelow (x "/\" y) and
A5: z in uparrow a ; ::_thesis: contradiction
reconsider z = z as Element of L by A4;
( z << x "/\" y & z >= a ) by A4, A5, WAYBEL_0:18, WAYBEL_3:7;
then a << x "/\" y by WAYBEL_3:2;
hence contradiction by A3, WAYBEL_4:def_1; ::_thesis: verum
end;
then waybelow (x "/\" y) misses uparrow a by XBOOLE_0:3;
then consider P being Ideal of L such that
A6: P is prime and
A7: waybelow (x "/\" y) c= P and
A8: P misses uparrow a by Th23;
set p = sup P;
sup P is pseudoprime by A6, Def6;
then A9: sup P is prime by A1;
a <= a ;
then A10: a in uparrow a by WAYBEL_0:18;
A11: ( x "/\" y = sup (waybelow (x "/\" y)) & ex_sup_of waybelow (x "/\" y),L ) by WAYBEL_0:75, WAYBEL_3:def_5;
ex_sup_of P,L by WAYBEL_0:75;
then x "/\" y <= sup P by A7, A11, YELLOW_0:34;
then ( ( x <= sup P & a << x ) or ( y <= sup P & a << y ) ) by A2, A9, WAYBEL_4:def_1, WAYBEL_6:def_6;
then a in P by WAYBEL_3:20;
hence contradiction by A8, A10, XBOOLE_0:3; ::_thesis: verum
end;