:: WAYBEL_7 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: WAYBEL_7:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WAYBEL_7:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: WAYBEL_7:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE
for X, Y being set st X c= Y holds
( "\/" X,L <= "\/" Y,L & "/\" X,L >= "/\" Y,L )
proof end;

theorem Th4: :: WAYBEL_7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds the carrier of (BoolePoset X) = bool X
proof end;

theorem Th5: :: WAYBEL_7:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty antisymmetric bounded RelStr holds
( L is trivial iff Top L = Bottom L )
proof 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 Boolean ;
coherence
not BoolePoset X is trivial
proof end;
end;

theorem :: WAYBEL_7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WAYBEL_7:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: WAYBEL_7:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
cluster non trivial strict Boolean RelStr ;
existence
ex b1 being LATTICE st
( not b1 is trivial & b1 is Boolean & b1 is strict )
proof end;
end;

registration
let X be set ;
cluster non empty finite Element of bool (bool X);
existence
ex b1 being Subset-Family of X st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
let S be 1-sorted ;
cluster non empty finite Element of bool (bool the carrier of S);
existence
ex b1 being Subset-Family of S st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
let L be non empty non trivial upper-bounded Poset;
cluster proper Element of bool the carrier of L;
existence
ex b1 being Filter of L st b1 is proper
proof end;
end;

theorem Th9: :: WAYBEL_7:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for a being Element of (BoolePoset X) holds 'not' a = X \ a
proof end;

theorem :: WAYBEL_7:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th11: :: WAYBEL_7:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th13: :: WAYBEL_7:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th15: :: WAYBEL_7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let L be with_infima Poset;
let I be Ideal of L;
attr I 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 Th16: :: WAYBEL_7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
let L be LATTICE;
cluster prime Element of bool the carrier of L;
existence
ex b1 being Ideal of L st b1 is prime
proof end;
end;

theorem :: WAYBEL_7:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let L be with_suprema Poset;
let F be Filter of L;
attr F 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:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
let L be LATTICE;
cluster prime Element of bool the carrier of L;
existence
ex b1 being Filter of L st b1 is prime
proof end;
end;

theorem Th19: :: WAYBEL_7:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th20: :: WAYBEL_7:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE
for x being set holds
( x is prime Ideal of L iff x is prime Filter of (L opp ) )
proof end;

theorem Th21: :: WAYBEL_7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE
for x being set holds
( x is prime Filter of L iff x is prime Ideal of (L opp ) )
proof end;

theorem :: WAYBEL_7:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE
for I being Ideal of L holds
( I is prime iff I in PRIME (InclPoset (Ids L)) )
proof end;

theorem Th24: :: WAYBEL_7:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th25: :: WAYBEL_7:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let L be non empty Poset;
let F be Filter of L;
attr F 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 ultra -> proper 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 end;

theorem Th26: :: WAYBEL_7:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Boolean LATTICE
for F being Filter of L holds
( ( F is proper & F is prime ) iff F is ultra )
proof 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 end;

theorem Th27: :: WAYBEL_7:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th28: :: WAYBEL_7:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th29: :: WAYBEL_7:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th30: :: WAYBEL_7:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let T be TopSpace;
let F, x be set ;
pred x 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;
pred x 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 proper ultra Element of bool the carrier of (BoolePoset X);
existence
ex b1 being Filter of (BoolePoset X) st b1 is ultra
proof end;
end;

theorem Th31: :: WAYBEL_7:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th32: :: WAYBEL_7:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th34: :: WAYBEL_7:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th37: :: WAYBEL_7:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE
for p being Element of L st p is prime holds
downarrow p is prime
proof end;

definition
let L be LATTICE;
let p be Element of L;
attr p 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 Th38: :: WAYBEL_7:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE
for p being Element of L st p is prime holds
p is pseudoprime
proof end;

theorem Th39: :: WAYBEL_7:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let L be non empty RelStr ;
let R be Relation of the carrier of L;
attr R 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;
cluster R -above x -> upper ;
coherence
R -above x is upper
proof end;
end;

theorem :: WAYBEL_7:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th45: :: WAYBEL_7:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being lower-bounded LATTICE
for R being auxiliary Relation of L holds
( R is multiplicative iff R -below is meet-preserving )
proof end;

Lm3: now
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 & not x <= p & not y <= p ) by A3, WAYBEL_6:def 6;
A5: 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
A6: ( u << x & not u <= p ) by A4, WAYBEL_3:24;
consider v being Element of L such that
A7: ( v << y & not v <= p ) by A4, A5, WAYBEL_3:24;
( [u,x] in L -waybelow & [v,y] in L -waybelow ) by A6, A7, WAYBEL_4:def 2;
then [(u "/\" v),(x "/\" y)] in L -waybelow by A1, Th45;
then u "/\" v << x "/\" y by WAYBEL_4:def 2;
then u "/\" v << p by A4, WAYBEL_3:2;
hence contradiction by A2, A6, A7; :: thesis: verum
end;

theorem Th48: :: WAYBEL_7:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: WAYBEL_7:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;